(*----------------------------------------------------------------------(C)-*)
(* Copyright (C) 2006 -2012 Konstantin Korovin and The University of Manchester.
   This file is part of iProver - a theorem prover for first - order logic.

   iProver is free software: you can redistribute it and / or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   (at your option) any later version.
   iProver is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
   See the GNU General Public License for more details.
   You should have received a copy of the GNU General Public License
   along with iProver. If not, see < http:// www.gnu.org / licenses />. *)
(*----------------------------------------------------------------------[C]-*)

open Lib

(* Option values with defaults and overrides from files or command-line *)

(* How to use these overrides: (assume an option named [opt])

 * Use type [ opt override ] for the type of the option

 * In the function set_new_current_options:
   [ opt = override o.opt !current_options.opt; ]

 * In op_fun:
   [ !current_options.opt <- override_cmd b !current_options.opt ]

 * In x_options_str_list:
   [ (opt_type_to_str (val_of_override opt.opt) ] ;

 * In the options:
   [ opt = ValueDefault 0; ]

 * When reading the options value:
   [ val_of_override !current_options.opt ]

 *)

(* An option set from different sources *)
type 'a override =
    
    (* Option has the default value *)
  | ValueDefault of 'a
	
	(* Default has been overridden by file argument *)
  | ValueFile of 'a
	
	(* Default has been overridden by command-line argument *)
  | ValueCmd of 'a

(* Get current value of option *)
let val_of_override = function
  | ValueDefault v -> v
  | ValueFile v -> v
  | ValueCmd v -> v

(* Override value with a new default value *)
let override_default v' = function
    
    (* Override previous default value *)
  | ValueDefault _ -> ValueDefault v'
	
	(* Do not override file or command line values *)
  | _ as v -> v

(* Override value with a new default value *)
let override_file v' = function
    
    (* Override previous default or file value *)
  | ValueDefault _
  | ValueFile _ -> ValueFile v'
	
	(* Do not override command line value *)
  | _ as v -> v

(* Override value with a new command-line value *)
let override_cmd v' = function
    
    (* Override previous default, file or command-line value  *)
  | ValueDefault _
  | ValueFile _
  | ValueCmd _ -> ValueCmd v'

(* Override one value with another *)
let override = function
  | ValueDefault v -> override_default v
  | ValueFile v -> override_file v
  | ValueCmd v -> override_cmd v

(* Change the value keeping its status *)
let override_value = function
  | ValueDefault _ -> (function v -> ValueDefault v)
  | ValueFile _ -> (function v -> ValueFile v)
  | ValueCmd _ -> (function v -> ValueCmd v)

(*--prase list options----*)
exception Parse_list_fail

let parse_list_opt str =
  let str_ln = String.length str in
  if (str.[0] = '[') & (str.[(str_ln -1)] = ']')
  then
    let new_str = String.sub str 1 (str_ln -2) in
    let str_list = Str.split (Str.regexp "[|;|]") new_str in
    str_list
  else
    raise Parse_list_fail

(*--parse functional options of form "fun_name[arg1;arg2;...]"---*)
(*--returns ("fun_name",["arg1";"arg2";...]--*)
exception Parse_fun_fail
let parse_fun_opt str =
  let br_reg_exp = Str.regexp "\\[\\([0-9]\\|[a-z]\\|[A-Z]\\|;\\)+\\]" in
  try
    let list_start = Str.search_forward br_reg_exp str 0 in
    let fun_str = String.sub str 0 list_start in
    out_str ("fun_str"^fun_str^"\n");
    let arg_str = Str.matched_string str in
    (fun_str, (parse_list_opt arg_str))
  with
  | Not_found | Parse_list_fail -> raise Parse_fun_fail

(*-----------------Option Types---------------------------*)

(*---------General----------*)
type out_options_type = Out_All_Opt | Out_Control_Opt | Out_No_Opt

let out_options_type_to_str opt =
  match opt with
  | Out_All_Opt -> "all"
  | Out_Control_Opt -> "control"
  | Out_No_Opt -> "none"

exception Unknown_out_options_type
let str_to_out_options_type str =
  match str with
  |"all" -> Out_All_Opt
  |"control" -> Out_Control_Opt
  |"none" -> Out_No_Opt
  | _ -> raise Unknown_out_options_type

(*--------*)
type ground_splitting_type = Split_Input | Split_Full | Split_Off

let ground_splitting_type_to_str opt =
  match opt with
  | Split_Input -> "input"
  | Split_Full -> "full"
  | Split_Off -> "off"

exception Unknown_ground_splitting_type
let str_to_ground_splitting_type str =
  match str with
  |"input" -> Split_Input
  |"full" -> Split_Full
  |"off" -> Split_Off
  | _ -> raise Unknown_ground_splitting_type

(*--------*)
type prep_sem_filter_type =
    Sem_Filter_None | Sem_Filter_Pos | Sem_Filter_Neg | Sem_Filter_Exhaustive

let prep_sem_filter_type_to_str opt =
  match opt with
  | Sem_Filter_None -> "none"
  | Sem_Filter_Pos -> "pos"
  | Sem_Filter_Neg -> "neg"
  | Sem_Filter_Exhaustive -> "exhaustive"

exception Unknown_sem_filter_type
let str_to_prep_sem_filter_type str =
  match str with
  |"none" -> Sem_Filter_None
  |"pos" -> Sem_Filter_Pos
  |"neg" -> Sem_Filter_Neg
  |"exhaustive" -> Sem_Filter_Exhaustive
  | _ -> raise Unknown_sem_filter_type

let prep_sem_filter_type_str = "<none|pos|neg|exhaustive>"

(*--------*)

(* Output no statistics, statistics after every bound or only after
   the last bound in BMC1 *)
type bmc1_out_stat_type =
    BMC1_Out_Stat_None | BMC1_Out_Stat_Full | BMC1_Out_Stat_Last

let bmc1_out_stat_type_to_str = function
  | BMC1_Out_Stat_None -> "none"
  | BMC1_Out_Stat_Full -> "full"
  | BMC1_Out_Stat_Last -> "last"

exception Unknown_bmc1_out_stat_type
let str_to_bmc1_out_stat_type = function
  | "none" -> BMC1_Out_Stat_None
  | "full" -> BMC1_Out_Stat_Full
  | "last" -> BMC1_Out_Stat_Last
  | _ -> raise Unknown_bmc1_out_stat_type

let bmc1_out_stat_type_list_str = "<none|full|last>"

(*--------*)

type bmc1_axioms_type =
    BMC1_Axioms_Reachable_All | BMC1_Axioms_Reachable_Last

let bmc1_axioms_type_to_str = function
  | BMC1_Axioms_Reachable_All -> "reachable_all"
  | BMC1_Axioms_Reachable_Last -> "reachable_last"

exception Unknown_bmc1_axioms_type
let str_to_bmc1_axioms_type = function
  | "reachable_all" -> BMC1_Axioms_Reachable_All
  | "reachable_last" -> BMC1_Axioms_Reachable_Last
  | _ -> raise Unknown_bmc1_axioms_type

let bmc1_axioms_type_list_str = "<reachable_all|reachable_last>"

(*--------*)

type bmc1_add_unsat_core_type =
  | BMC1_Add_Unsat_Core_None
  | BMC1_Add_Unsat_Core_Clauses
  | BMC1_Add_Unsat_Core_Leaves
  | BMC1_Add_Unsat_Core_All

let bmc1_add_unsat_core_type_to_str = function
  | BMC1_Add_Unsat_Core_None -> "none"
  | BMC1_Add_Unsat_Core_Clauses -> "clauses"
  | BMC1_Add_Unsat_Core_Leaves -> "leaves"
  | BMC1_Add_Unsat_Core_All -> "all"

exception Unknown_bmc1_add_unsat_core_type
let str_to_bmc1_add_unsat_core_type = function
  | "none" -> BMC1_Add_Unsat_Core_None
  | "clauses" -> BMC1_Add_Unsat_Core_Clauses
  | "leaves" -> BMC1_Add_Unsat_Core_Leaves
  | "all" -> BMC1_Add_Unsat_Core_All
  | _ -> raise Unknown_bmc1_add_unsat_core_type

let bmc1_add_unsat_core_type_list_str = "<none|leaves|clauses|all>"

(*--------*)

type schedule_type =
  | Schedule_none
  | Schedule_default
  | Schedule_sat
  | Schedule_verification_epr
  | Schedule_verification_epr_tables

let schedule_type_to_str opt =
  match opt with
  | Schedule_none -> "none"
  | Schedule_default -> "default"
  | Schedule_sat -> "sat"
  | Schedule_verification_epr -> "verification_epr"
  | Schedule_verification_epr_tables -> "verification_epr_tables"

exception Unknown_schedule_type
let str_to_schedule_type str =
  match str with
  |"none" -> Schedule_none
  |"default" -> Schedule_default
  |"sat" -> Schedule_sat
  |"verification_epr" -> Schedule_verification_epr
  |"verification_epr_tables" -> Schedule_verification_epr_tables
  | _ -> raise Unknown_schedule_type

let schedule_type_list_str ="<none|default|sat|verification_epr|verification_epr_tables>"

(*-----Lit Params----------*)

type lit_cmp_type =
  | Lit_Sign of bool
  | Lit_Ground of bool
  | Lit_Num_of_Var of bool
  | Lit_Num_of_Symb of bool
  | Lit_Atom_depth of bool
  | Lit_Split of bool
  | Lit_has_conj_symb of bool
  | Lit_has_bound_constant of bool
  | Lit_next_state of bool
  | Lit_reachable_state of bool
	(*  | Lit_reachable_state            of bool *)
  | Lit_has_non_prolific_conj_symb of bool
  | Lit_eq of bool
  | Lit_clock of bool
  | Lit_less of bool
  | Lit_range of bool

let lit_cmp_type_to_str par =
  match par with
  | Lit_Sign b -> if b then "+sign" else "-sign"
  | Lit_Ground b -> if b then "+ground" else "-ground"
  | Lit_Num_of_Var b -> if b then "+num_var" else "-num_var"
  | Lit_Num_of_Symb b -> if b then "+num_symb" else "-num_symb"
  | Lit_Atom_depth b -> if b then "+depth" else "-depth"
  | Lit_Split b -> if b then "+split" else "-split"
  | Lit_has_conj_symb b -> if b then "+conj_symb" else "-conj_symb"
  | Lit_has_bound_constant b -> if b then "+has_bound_constant" else "-has_bound_constant"
  | Lit_next_state b -> if b then "+next_state" else "-next_state"
  | Lit_reachable_state b -> if b then "+reachable_state" else "-reachable_state"
  | Lit_has_non_prolific_conj_symb b ->
      if b then "+non_prol_conj_symb" else "-non_prol_conj_symb"
  | Lit_eq b -> if b then "+eq" else "-eq"
  | Lit_clock b -> if b then "+clock" else "-clock"
  | Lit_less b -> if b then "+less" else "-less"
  | Lit_range b -> if b then "+range" else "-range"

exception Unknown_lit_cmp_type
let str_to_lit_cmp_type str =
  match str with
  | "+sign" -> Lit_Sign true
  | "-sign" -> Lit_Sign false
  | "+ground" -> Lit_Ground true
  | "-ground" -> Lit_Ground false
  | "+num_var" -> Lit_Num_of_Var true
  | "-num_var" -> Lit_Num_of_Var false
  | "+num_symb" -> Lit_Num_of_Symb true
  | "-num_symb" -> Lit_Num_of_Symb false
  | "+depth" -> Lit_Atom_depth true
  | "-depth" -> Lit_Atom_depth false
  | "+split" -> Lit_Split true
  | "-split" -> Lit_Split false
  | "+conj_symb" -> Lit_has_conj_symb true
  | "-conj_symb" -> Lit_has_conj_symb false
  | "+has_bound_constant" -> Lit_has_bound_constant true
  | "-has_bound_constant" -> Lit_has_bound_constant false
  | "+next_state" -> Lit_next_state true
  | "-next_state" -> Lit_next_state false
  | "+reachable_state" -> Lit_reachable_state true
  | "-reachable_state" -> Lit_reachable_state false
  | "+non_prol_conj_symb" -> Lit_has_non_prolific_conj_symb true
  | "-non_prol_conj_symb" -> Lit_has_non_prolific_conj_symb false
  | "+eq" -> Lit_eq true
  | "-eq" -> Lit_eq false
  | "+clock" -> Lit_clock true
  | "-clock" -> Lit_clock false
  | "+less" -> Lit_less true
  | "-less" -> Lit_less false
  | "+range" -> Lit_range true
  | "-range" -> Lit_range false
  | _ -> raise Unknown_lit_cmp_type

let lit_cmp_type_list_str = "<[((+|-)(sign|ground|num_var|num_symb|depth|split|conj_symb|non_prol_conj_symb|eq|clock|less|range|has_bound_constant|next_state|reachable_state)^+]>"

(* if there is no conjectures then we can to remove corresponding comparisons*)

let strip_conj_lit_type_list lit_type_list =
  let rec strip' rest list =
    match list with
    | h:: tl ->
	(match h with
	| Lit_has_conj_symb _ -> strip' rest tl
	| Lit_has_non_prolific_conj_symb _ -> strip' rest tl
	| _ -> strip' (h:: rest) tl
	)
    |[] -> List.rev rest
  in
  strip' [] lit_type_list

(*----Clause Param---------*)
type cl_cmp_type =
  | Cl_Age of bool
  | Cl_Num_of_Var of bool
  | Cl_Num_of_Symb of bool
  | Cl_Num_of_Lits of bool
  | Cl_Ground of bool
  | Cl_Conj_Dist of bool
  | Cl_Has_Conj_Symb of bool
  | Cl_has_bound_constant of bool
  | Cl_has_next_state of bool
  | Cl_has_reachable_state of bool
  | Cl_Has_Non_Prolific_Conj_Symb of bool
  | Cl_Max_Atom_Input_Occur of bool
  | Cl_Horn of bool
  | Cl_EPR of bool
  | Cl_in_unsat_core of bool
  | Cl_Has_Eq_Lit of bool
	(* defined symbols as in father_of relatio (Intel) *)
  | Cl_min_defined_symb of bool

let cl_cmp_type_to_str par =
  match par with
  | Cl_Age b -> if b then "+age" else "-age"
  | Cl_Num_of_Var b -> if b then "+num_var" else "-num_var"
  | Cl_Num_of_Symb b -> if b then "+num_symb" else "-num_symb"
  | Cl_Num_of_Lits b -> if b then "+num_lits" else "-num_lits"
  | Cl_Ground b -> if b then "+ground" else "-ground"
  | Cl_Conj_Dist b -> if b then "+conj_dist" else "-conj_dist"
  | Cl_Has_Conj_Symb b -> if b then "+conj_symb" else "-conj_symb"
  | Cl_has_bound_constant b -> if b then "+has_bound_constant" else "-has_bound_constant"
  | Cl_has_next_state b -> if b then "+next_state" else "-next_state"
  | Cl_has_reachable_state b -> if b then "+reachable_state" else "-reachable_state"
  | Cl_Has_Non_Prolific_Conj_Symb b -> if b then "+conj_non_prolific_symb" else "-conj_non_prolific_symb"
  | Cl_Max_Atom_Input_Occur b -> if b then "+max_atom_input_occur" else
    "-max_atom_input_occur"
  | Cl_Horn b -> if b then "+horn" else "-horn"
  | Cl_EPR b -> if b then "+epr" else "-epr"
  | Cl_in_unsat_core b -> if b then "+uc" else "-uc"
  | Cl_Has_Eq_Lit b -> if b then "+has_eq" else "-has_eq"
  | Cl_min_defined_symb b -> if b then "+min_def_symb" else "-min_def_symb"

exception Unknown_cl_cmp_type
let str_to_cl_cmp_type str =
  match str with
  |"+age" -> Cl_Age true
  |"-age" -> Cl_Age false
  |"+num_var" -> Cl_Num_of_Var true
  |"-num_var" -> Cl_Num_of_Var false
  |"+num_symb" -> Cl_Num_of_Symb true
  |"-num_symb" -> Cl_Num_of_Symb false
  |"+num_lits" -> Cl_Num_of_Lits true
  |"-num_lits" -> Cl_Num_of_Lits false
  |"+ground" -> Cl_Ground true
  |"-ground" -> Cl_Ground false
  |"+conj_dist" -> Cl_Conj_Dist true
  |"-conj_dist" -> Cl_Conj_Dist false
  |"+has_bound_constant" -> Cl_has_bound_constant true
  |"-has_bound_constant" -> Cl_has_bound_constant false
  |"+next_state" -> Cl_has_next_state true
  |"-next_state" -> Cl_has_next_state false
  |"+reachable_state" -> Cl_has_reachable_state true
  |"-reachable_state" -> Cl_has_reachable_state false
  |"+conj_symb" -> Cl_Has_Conj_Symb true
  |"-conj_symb" -> Cl_Has_Conj_Symb false
  |"+conj_non_prolific_symb" -> Cl_Has_Non_Prolific_Conj_Symb true
  |"-conj_non_prolific_symb" -> Cl_Has_Non_Prolific_Conj_Symb false
  |"+max_atom_input_occur" -> Cl_Max_Atom_Input_Occur true
  |"-max_atom_input_occur" -> Cl_Max_Atom_Input_Occur false
  |"+horn" -> Cl_Horn true
  |"-horn" -> Cl_Horn false
  |"+epr" -> Cl_EPR true
  |"-epr" -> Cl_EPR false
  |"+uc" -> Cl_in_unsat_core true
  |"-uc" -> Cl_in_unsat_core false
  |"+has_eq" -> Cl_Has_Eq_Lit true
  |"-has_eq" -> Cl_Has_Eq_Lit false
  |"+min_def_symb" -> Cl_min_defined_symb true
  |"-min_def_symb" -> Cl_min_defined_symb false
  | _ -> raise Unknown_cl_cmp_type

let cl_cmp_type_list_str = "<[((+|-)(age|num_var|num_symb|num_lits|ground|conj_dist|conj_symb|max_atom_input_occur|horn|epr|uc|has_eq|has_bound_constant|min_def_symb|next_state|reachable_state)^+]>"

let strip_conj_clause_type_list clause_type_list =
  let rec strip' rest list =
    match list with
    | h:: tl ->
	(match h with
	| Cl_Conj_Dist _ -> strip' rest tl
	| Cl_Has_Conj_Symb _ -> strip' rest tl
	| Cl_Has_Non_Prolific_Conj_Symb _ -> strip' (h:: rest) tl
	| _ -> strip' (h:: rest) tl
	)
    |[] -> List.rev rest
  in
  strip' [] clause_type_list

(*--------------------Instantiation Option Types--------------*)

(*---Inst Lit Sel----*)

type inst_lit_sel_type = lit_cmp_type list

let inst_lit_sel_type_to_str t =
  ("["^(list_to_string lit_cmp_type_to_str t ";")^"]")

type pass_queue_type = cl_cmp_type list

let pass_queue_type_to_str t =
  ("["^(list_to_string cl_cmp_type_to_str t ";")^"]")

type inst_sel_renew_type = Inst_SR_Solver | Inst_SR_Model

let inst_sel_renew_type_to_str opt =
  match opt with
  | Inst_SR_Solver -> "solver"
  | Inst_SR_Model -> "model"

exception Unknown_inst_sel_renew_type
let str_to_inst_sel_renew_type str =
  match str with
  |"solver" -> Inst_SR_Solver
  |"model" -> Inst_SR_Model
  | _ -> raise Unknown_inst_sel_renew_type

(*---------------------sat_out_model option types-----------------------------------*)

type sat_out_model_type = Model_Small | Model_Pos | Model_Neg | Model_Implied | Model_Debug | Model_Intel | Model_None

let sat_out_model_type_to_str opt =
  match opt with
  | Model_Small -> "small"
  | Model_Pos -> "pos"
  | Model_Neg -> "neg"
  | Model_Implied -> "implied"
  | Model_Debug -> "debug"
  | Model_Intel -> "intel"
  | Model_None -> "none"

exception Unknown_sat_model_out_type
let str_to_sat_out_model_type str =
  match str with
  |"small" -> Model_Small
  |"pos" -> Model_Pos
  |"neg" -> Model_Neg
  |"implied" -> Model_Implied
  |"none" -> Model_None
  |"debug" -> Model_Debug
  |"intel" -> Model_Intel
  | _ -> raise Unknown_sat_model_out_type

let sat_out_model_type_str = "<small|pos|neg|implied|debug|intel|none>"

(*--------------------Resolution Option Types--------------*)

(*----Subsumption----*)
type res_subs_type = Subs_Full | Subs_Subset | Subs_By_Length of int

let res_subs_type_to_str t =
  match t with
  | Subs_Full -> "full"
  | Subs_Subset -> "subset_subsumption"
  | Subs_By_Length l ->
      ("length["^(string_of_int l)^"]")

exception Unknown_res_subs_type
let str_to_res_subs_type str =
  match str with
  |"full" -> Subs_Full
  |"subset_subsumption" -> Subs_Subset
  | str ->
      try
	let (fun_str, arg_list) = parse_fun_opt str in
	match fun_str with
	|"length" ->
	    (match arg_list with
	    |[num_str] -> Subs_By_Length (int_of_string num_str)
	    | _ -> failwith "str_to_res_subs_type wrong args"
	    )
	| _ -> raise Unknown_res_subs_type
      with
	Parse_fun_fail -> raise Unknown_res_subs_type

let res_subs_type_str = "<full | subset_subsumption | length[<int>]>"

(*---Selection Fun----*)

type res_lit_sel_type =
    Res_Adaptive | Res_KBO_Max | Res_Neg_Sel_Max | Res_Neg_Sel_Min

let res_lit_sel_type_to_str res_sel_type =
  match res_sel_type with
  | Res_Adaptive -> "adaptive"
  | Res_KBO_Max -> "kbo_max"
  | Res_Neg_Sel_Max -> "neg_max"
  | Res_Neg_Sel_Min -> "neg_min"

exception Unknown_res_sel_fun_type
let str_to_sel_type str =
  match str with
  |"adaptive" -> Res_Adaptive
  |"kbo_max" -> Res_KBO_Max
  |"neg_max" -> Res_Neg_Sel_Max
  |"neg_min" -> Res_Neg_Sel_Min
  | _ -> raise Unknown_res_sel_fun_type

(*-----*)

type res_to_prop_solver_type =
    Res_to_Solver_Active | Res_to_Solver_Passive | Res_to_Solver_None

let res_to_prop_solver_type_to_str t =
  match t with
  | Res_to_Solver_Active -> "active"
  | Res_to_Solver_Passive -> "passive"
  | Res_to_Solver_None -> "none"

exception Unknown_res_to_prop_solver_type
let str_to_res_to_prop_solver_type str =
  match str with
  |"active" -> Res_to_Solver_Active
  |"passive" -> Res_to_Solver_Passive
  |"none" -> Res_to_Solver_None
  | _ -> raise Unknown_res_to_prop_solver_type

(*-----All options-----*)

type options = {
    mutable out_options : out_options_type override;
    mutable tptp_safe_out : bool;
    
    (*----Input-------*)
    mutable problem_path : string;
    mutable include_path : string;
    mutable problem_files : string list;
    mutable clausifier : string;
    mutable clausifier_options : string;
    mutable stdin : bool;
    mutable dbg_backtrace : bool;
    mutable dbg_dump_prop_clauses : bool;
    mutable dbg_dump_prop_clauses_file : string;
    mutable dbg_out_stat : bool;
    
    (*----General--------*)
    mutable fof : bool;
    mutable time_out_real : float;
    mutable time_out_virtual : float;
    mutable schedule : schedule_type;
    mutable ground_splitting : ground_splitting_type;
    mutable non_eq_to_eq : bool;
    mutable prep_gs_sim : bool;
    mutable prep_res_sim : bool;
    mutable res_sim_input : bool;
    mutable clause_weak_htbl: bool;
    mutable gc_record_bc_elim: bool;
    mutable symbol_type_check : bool;
    mutable clausify_out : bool;
    mutable prep_sem_filter : prep_sem_filter_type;
    mutable prep_sem_filter_out : bool;
    mutable sub_typing : bool;
    mutable brand_transform : bool;
    mutable min_unsat_core : bool;
    
    (*---Large Theories---------------*)
    mutable large_theory_mode : bool;
    
    mutable prolific_symb_bound : int;
    mutable lt_threshold : int;
    
    (*----Sat Mode-----------*)
    mutable sat_mode : bool;
    mutable sat_gr_def : bool;
    mutable sat_epr_types : bool;
    mutable sat_non_cyclic_types : bool;
    mutable sat_finite_models : bool;
    mutable sat_out_model : sat_out_model_type;
    mutable sat_out_clauses : bool;
    
    (*----BMC1---------------*)
    mutable bmc1_incremental : bool override;
    mutable bmc1_axioms : bmc1_axioms_type override;
    mutable bmc1_min_bound : int override;
    mutable bmc1_max_bound : int override;
    mutable bmc1_max_bound_default : int override;
    mutable bmc1_symbol_reachability : bool;
    mutable bmc1_add_unsat_core : bmc1_add_unsat_core_type override;
    mutable bmc1_unsat_core_children : bool override;
    mutable bmc1_unsat_core_extrapolate_axioms : bool override;
    mutable bmc1_pre_inst_next_state : bool;
    mutable bmc1_pre_inst_state : bool;
    mutable bmc1_pre_inst_reach_state : bool;
    mutable bmc1_out_stat : bmc1_out_stat_type override;
    mutable bmc1_out_unsat_core : bool override;
    mutable bmc1_verbose : bool override;
    mutable bmc1_dump_clauses_tptp : bool override;
    mutable bmc1_dump_unsat_core_tptp : bool override;
    mutable bmc1_dump_file : string option override;
    
    (*----Instantiation------*)
    mutable instantiation_flag : bool;
    mutable inst_lit_sel : inst_lit_sel_type;
    mutable inst_solver_per_active : int;
    mutable inst_solver_per_clauses : int;
    mutable inst_pass_queue1 : pass_queue_type override;
    mutable inst_pass_queue2 : pass_queue_type override;
    mutable inst_pass_queue3 : pass_queue_type override;
    mutable inst_pass_queue1_mult : int override;
    mutable inst_pass_queue2_mult : int override;
    mutable inst_pass_queue3_mult : int override;
    mutable inst_dismatching : bool;
    mutable inst_eager_unprocessed_to_passive : bool;
    mutable inst_prop_sim_given : bool;
    mutable inst_prop_sim_new : bool;
    mutable inst_orphan_elimination : bool;
    mutable inst_learning_loop_flag : bool;
    mutable inst_learning_start : int;
    mutable inst_learning_factor : int;
    mutable inst_start_prop_sim_after_learn : int;
    mutable inst_sel_renew : inst_sel_renew_type;
    mutable inst_lit_activity_flag : bool;
    mutable inst_out_proof : bool override;
    
    (*----Resolution---------*)
    mutable resolution_flag : bool;
    mutable res_lit_sel : res_lit_sel_type;
    mutable res_to_prop_solver : res_to_prop_solver_type;
    mutable res_prop_simpl_new : bool;
    mutable res_prop_simpl_given : bool;
    
    mutable res_passive_queue_flag : bool;
    mutable res_pass_queue1 : pass_queue_type;
    mutable res_pass_queue2 : pass_queue_type;
    mutable res_pass_queue1_mult : int;
    mutable res_pass_queue2_mult : int;
    
    mutable res_forward_subs : res_subs_type;
    mutable res_backward_subs : res_subs_type;
    mutable res_forward_subs_resolution : bool;
    mutable res_backward_subs_resolution : bool;
    mutable res_orphan_elimination : bool;
    mutable res_time_limit : float;
    mutable res_out_proof : bool;
    (*----Combination--------*)
    mutable comb_res_mult : int;
    mutable comb_inst_mult : int;
  }

let default_options () = {

  out_options = ValueDefault Out_All_Opt;
  tptp_safe_out = false;
  
  (*----Input-------*)
  problem_path = "";
  include_path = "";
  problem_files = [];
  clausifier = "";
  clausifier_options = "";
  stdin = false;
  dbg_backtrace = false;
  dbg_dump_prop_clauses = false;
  dbg_dump_prop_clauses_file = "-";
  dbg_out_stat = false; 
  
  (*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = Schedule_default;
  ground_splitting = Split_Input;
  non_eq_to_eq = false;
  prep_gs_sim = true;
  prep_res_sim = true;
  res_sim_input = true;
  clause_weak_htbl = true;
  gc_record_bc_elim = false;
  symbol_type_check = false;
  clausify_out = false;
  (*  prep_sem_filter         = Sem_Filter_None;*)
  prep_sem_filter = Sem_Filter_Exhaustive;
  prep_sem_filter_out = false;
  (*  sub_typing              = false;*)
  sub_typing = true;
  brand_transform = false;
  min_unsat_core = false;
  
  (*---Large Theories---------------*)
  large_theory_mode = true;
  
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*---Sat mode------------*)
  sat_mode = false;
  sat_epr_types = true;
  sat_non_cyclic_types = false;
  sat_gr_def = false;
  sat_finite_models = false;
  sat_out_model = Model_Small;
  sat_out_clauses = false;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  (*bmc1_symbol_reachability should be modified only by input options and not by options in schedule since it is calculated before options in schedule become active *)
  bmc1_symbol_reachability = true;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----Instantiation------*)
  instantiation_flag = true;
  inst_lit_sel = [Lit_Sign true; Lit_Ground true;
		  Lit_Num_of_Var false; Lit_Num_of_Symb false];
  
  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  
  inst_pass_queue1 =
  ValueDefault
    [Cl_Conj_Dist false;
     Cl_Has_Conj_Symb true;
     Cl_Num_of_Var false];
  
  inst_pass_queue2 =
  ValueDefault
    [Cl_Age true;
     Cl_Num_of_Symb false];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 25;
  (* inst_pass_queue2_mult = 2; before 29 Aug 2011 changed for Zurab's dcu default *)
  inst_pass_queue2_mult = ValueDefault 2;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  inst_dismatching = true;
  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = true;
  inst_orphan_elimination = true;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Model;
  inst_lit_activity_flag = true;
  inst_out_proof = ValueDefault true;
  
  (*----Resolution---------*)
  resolution_flag = true;
  res_lit_sel = Res_Adaptive;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Conj_Dist false; Cl_Has_Conj_Symb true;
		     Cl_Num_of_Symb false];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 5;
  
  res_forward_subs = Subs_Full;
  res_backward_subs = Subs_Full;
  res_forward_subs_resolution = true;
  res_backward_subs_resolution = true;
  res_orphan_elimination = true;
  res_time_limit = 2.0;
  res_out_proof = true;
  (*----Combination--------*)
  comb_res_mult = 300;
  comb_inst_mult = 1000;
}

(*---------*)
let current_options = ref (default_options ())

let set_new_current_options o =
  current_options :=
    { o with
      
      (* Only override defaults *)
      out_options =
      override o.out_options !current_options.out_options;
      
      (* Only override defaults *)
      bmc1_incremental =
      override o.bmc1_incremental !current_options.bmc1_incremental;
      
      (* Only override defaults *)
      bmc1_axioms =
      override o.bmc1_axioms !current_options.bmc1_axioms;
      
      (* Only override defaults *)
      bmc1_min_bound =
      override o.bmc1_min_bound !current_options.bmc1_min_bound;
      
      (* Only override defaults *)
      bmc1_max_bound =
      override o.bmc1_max_bound !current_options.bmc1_max_bound;
      
      (* Only override defaults *)
      bmc1_max_bound_default =
      override
	o.bmc1_max_bound_default
	!current_options.bmc1_max_bound_default;
      
      (* Only override defaults *)
      bmc1_add_unsat_core =
      override o.bmc1_add_unsat_core !current_options.bmc1_add_unsat_core;
      
      (* Only override defaults *)
      bmc1_unsat_core_children =
      override
	o.bmc1_unsat_core_children
	!current_options.bmc1_unsat_core_children;
      
      (* Only override defaults *)
      bmc1_unsat_core_extrapolate_axioms =
      override
	o.bmc1_unsat_core_extrapolate_axioms
	!current_options.bmc1_unsat_core_extrapolate_axioms;
      
      (* Only override defaults *)
      bmc1_out_stat =
      override o.bmc1_out_stat !current_options.bmc1_out_stat;
      
      (* Only override defaults *)
      bmc1_out_unsat_core =
      override o.bmc1_out_unsat_core !current_options.bmc1_out_unsat_core;
      
      (* Only override defaults *)
      bmc1_verbose =
      override o.bmc1_verbose !current_options.bmc1_verbose;
      
      (* Only override defaults *)
      bmc1_dump_clauses_tptp =
      override
	o.bmc1_dump_clauses_tptp
	!current_options.bmc1_dump_clauses_tptp;
      
      (* Only override defaults *)
      bmc1_dump_unsat_core_tptp =
      override
	o.bmc1_dump_unsat_core_tptp
	!current_options.bmc1_dump_unsat_core_tptp;
      
      (* Only override defaults *)
      bmc1_dump_file =
      override o.bmc1_dump_file !current_options.bmc1_dump_file;
      
      (* Only override defaults *)
      inst_pass_queue1 =
      override o.inst_pass_queue1 !current_options.inst_pass_queue1;
      
      (* Only override defaults *)
      inst_pass_queue2 =
      override o.inst_pass_queue2 !current_options.inst_pass_queue2;
      
      (* Only override defaults *)
      inst_pass_queue3 =
      override o.inst_pass_queue3 !current_options.inst_pass_queue3;
      
      (* Only override defaults *)
      inst_pass_queue1_mult =
      override
	o.inst_pass_queue1_mult
	!current_options.inst_pass_queue1_mult;
      
      (* Only override defaults *)
      inst_pass_queue2_mult =
      override
	o.inst_pass_queue2_mult
	!current_options.inst_pass_queue2_mult;
      
      (* Only override defaults *)
      inst_pass_queue3_mult =
      override
	o.inst_pass_queue3_mult
	!current_options.inst_pass_queue3_mult;
      
      (* Only override defaults *)
      inst_out_proof =
      override
	o.inst_out_proof
	!current_options.inst_out_proof;
      
    }

(*---------*)
let args_error_msg opt_name str =
  ("Input Options: "^opt_name^" unsupported value \'"^str^"\'")

let add_file_options file_name =
  !current_options.problem_files <- file_name:: (!current_options.problem_files)

let default_arg_fun = add_file_options

(*---------------------Preparing for Args:---------------*)
(* 1. option name  ---*)
(* 2. functions for assigning options------*)
(* 3. description  ---*)
(*-------------------------------*)
let bool_str = "<bool>"
let string_str = "<string>"
let int_str = "<int>"
let float_str = "<float>"
let inf_pref = "\n    "
let example_str = inf_pref^"Example: "

(*-----*)
let out_options_str = "--out_options"

let out_options_fun str =
  try
    !current_options.out_options <-
      override_cmd (str_to_out_options_type str) !current_options.out_options
  with
    Unknown_out_options_type ->
      failwith (args_error_msg out_options_str str)

let out_options_inf =
  "<all | control | none>"^
  inf_pref^"controls output of options \n"

(*--------*)
let tptp_safe_out_str = "--tptp_safe_out"

let tptp_safe_out_fun b =
  Lib.tptp_safe_out_ref:= b;
  !current_options.tptp_safe_out <- b

let tptp_safe_out_inf =
  bool_str^"output all info strings as tptp comments"

(*----Input-------*)

let problem_path_str = "--problem_path"

let problem_path_fun str =
  !current_options.problem_path <- str

let problem_path_inf =
  string_str^
  example_str^problem_path_str^" /home/TPTP/Problems/PUZ/\n"

(*--------*)
let include_path_str = "--include_path"

let include_path_fun str =
  !current_options.include_path <- str

let include_path_inf =
  string_str^
  example_str^include_path_str^" /home/TPTP/\n"

(*--------*)

let clausifier_str = "--clausifier"

let clausifier_fun str =
  !current_options.clausifier <- str

let clausifier_inf =
  string_str^
  inf_pref^"if the input is in cnf this option is ignored"^
  inf_pref^"clausifier is assumed to read fof formulas from stdin and output clauses into stdout"^
  inf_pref^"(see also --clausifier_options)."^
  example_str^"iproveropt --clausifier eprover --clausifier_options \"--tstp-format \" problem.p"^
  inf_pref^"alternatevly, you can use environment variables CLAUSIFIER and CLAUSIFIER_OPTIONS\n"

(*--------*)

let clausifier_options_str = "--clausifier_options"

let clausifier_options_fun str =
  !current_options.clausifier_options <- str

let clausifier_options_inf =
  string_str^
  inf_pref^"options passed to clausifier (see --clausifier)\n"

(*--------*)
let stdin_str = "--stdin"

let stdin_fun bool =
  !current_options.stdin <- bool

let stdin_inf =
  bool_str^
  inf_pref^"read the problem from stdin,"^
  inf_pref^"if the problem is in fof then add \"--fof true\" flag \n"^
  (* ugly hack*)
  (dash_str "General Options")^"\n"

(*--------*)
let dbg_backtrace_str = "--dbg_backtrace"

let dbg_backtrace_fun b =
  (if b
  then
    Printexc.record_backtrace b
  else());
  !current_options.dbg_backtrace <- b

let dbg_backtrace_inf =
  bool_str^
  inf_pref^"debug: backtrace is recorderd and displayed, make iProver with \"make debug=true\" \n"

(*--------*)
let dbg_dump_prop_clauses_str = "--dbg_dump_prop_clauses"

let dbg_dump_prop_clauses_fun b =
  !current_options.dbg_dump_prop_clauses <- b

let dbg_dump_prop_clauses_inf =
  bool_str^
  inf_pref^"debug: dump propositional clauses into stderr\n"

(*--------*)
let dbg_dump_prop_clauses_file_str = "--dbg_dump_prop_clauses_file"

let dbg_dump_prop_clauses_file_fun b =
  !current_options.dbg_dump_prop_clauses_file <- b

let dbg_dump_prop_clauses_file_inf =
  bool_str^
  inf_pref^"debug: file to dump propositional clauses tp, use - for stdout\n"

(*--------*)
let dbg_out_stat_str = "--dbg_out_stat"

let dbg_out_stat_fun b =
  !current_options.dbg_out_stat <- b 

let dbg_out_stat_inf =  
  "debug: output statistics before proving \n"

(*----General--------*)

let fof_str = "--fof"

let fof_fun b =
  !current_options.fof <- b

let fof_inf =
  bool_str^
  inf_pref^"if false then it is assumed that the input is in cnf"^
  inf_pref^"if true then full first-order syntax is accepted"^
  inf_pref^"in the latter case --clausifier is used for clausification,"^
  inf_pref^"unless --stdin is true fof true/false is recognized automatically\n"

(*--------*)
let time_out_real_str = "--time_out_real"

let time_out_real_fun f =
  !current_options.time_out_real <- f

let time_out_real_inf =
  float_str^
  inf_pref^"time out in real time, if <0. then no time limit is imposed (in real time) \n"

(*--------*)
let time_out_virtual_str = "--time_out_virtual"

let time_out_virtual_fun f =
  !current_options.time_out_virtual <- f

let time_out_virtual_inf =
  float_str^
  inf_pref^"time out in virtual time, if <0. then no time limit is imposed (in virtual time) \n"

(*--------*)
let schedule_str = "--schedule"

let schedule_fun str =
  try
    !current_options.schedule <- str_to_schedule_type str
  with
    Unknown_schedule_type ->
      failwith (args_error_msg schedule_str str)

let schedule_inf =
  schedule_type_list_str^
  inf_pref^"run a specified strategy schedule:"^
  inf_pref^"\"default\" is the default schedule, works well over whole TPTP"^
  inf_pref^"\"none\" run just the input options, without a schedule"^
  inf_pref^"\"verification_epr\" a schedule which works well for verification problems encoded in the EPR fragment"^
  inf_pref^"in the future there will be an interface for the schedule to be read from an option file\n"

(*--------*)
let ground_splitting_str = "--ground_splitting"

let ground_splitting_fun str =
  try
    !current_options.ground_splitting <- (str_to_ground_splitting_type str)
  with
    Unknown_ground_splitting_type ->
      failwith (args_error_msg ground_splitting_str str)

let ground_splitting_inf =
  "<input | full | off >"^
  inf_pref^"splitting of clauses on maximal variable-disjoint parts\n"

(*--------*)

let non_eq_to_eq_str = "--non_eq_to_eq"

let non_eq_to_eq_fun b =
  !current_options.non_eq_to_eq <- b

let non_eq_to_eq_inf =
  bool_str^
  inf_pref^"replace all non-equational predicates with equational"^
  inf_pref^"e.g. p with f_p = top and  ~p with f_p != top\n"

(*--------*)

(*--------*)
let prep_gs_sim_str = "--prep_gs_sim"

let prep_gs_sim_fun b =
  !current_options.prep_gs_sim <- b

let prep_gs_sim_inf =
  bool_str^
  inf_pref^"simplify input first-order clauses using propositional solver by global subsumption\n"

(*--------*)
let prep_res_sim_str = "--prep_res_sim" 

let prep_res_sim_fun b = 
  !current_options.prep_res_sim <- b
      
let prep_res_sim_inf =
  bool_str^
  inf_pref^"preprocess simplification using resolution type simplifications such as subsumtion, subsumption resolution, etc.\n"

(*--------*)
let clause_weak_htbl_str = "--clause_weak_htbl" 

let clause_weak_htbl_fun b =
  !current_options.clause_weak_htbl <- b

let clause_weak_htbl_inf =
  bool_str^
  inf_pref^"use weak hash table to store all basic clauses; should not be switched in schedules\n"

(*--------*)
let gc_record_bc_elim_str = "--gc_record_bc_elim"

let gc_record_bc_elim_fun b = 
  !current_options.gc_record_bc_elim <- b

let gc_record_bc_elim_inf = 
  bool_str^
  inf_pref^"record the number of eliminated clauses by the garbage collector in gc_basic_clause_elim; only when --clause_weak_htbl true\n"

(*--------*)
let res_sim_input_str = "--res_sim_input"

let res_sim_input_fun b = 
  !current_options.res_sim_input <- b
      
let res_sim_input_inf =
  bool_str^
  inf_pref^"after a reseolution run, simplify input clauses for the next iterations of inst/res\n"


(*--------*)
let symbol_type_check_str = "--symbol_type_check"

let symbol_type_check_fun b =
  !current_options.symbol_type_check <- b

let symbol_type_check_inf =
  bool_str^
  inf_pref^"if true then it is checked whether there is no symbols with the same name and different types\n"

(*-------*)
let clausify_out_str = "--clausify_out"

let clausify_out_fun b =
  !current_options.clausify_out <- b

let clausify_out_inf =
  bool_str^
  inf_pref^"output the clausifier output and exit\n"

(*-------*)
let prep_sem_filter_str = "--prep_sem_filter"

let prep_sem_filter_fun str =
  try
    !current_options.prep_sem_filter <- (str_to_prep_sem_filter_type str)
  with
    Unknown_sem_filter_type ->
      failwith (args_error_msg prep_sem_filter_str str)

let prep_sem_filter_inf =
  prep_sem_filter_type_str^
  inf_pref^"apply semantic filter to the input clauses \n"

(*-------*)
let prep_sem_filter_out_str = "--prep_sem_filter_out"

let prep_sem_filter_out_fun b =
  !current_options.prep_sem_filter_out <- b

let prep_sem_filter_out_inf =
  bool_str^
  inf_pref^"semantic preproscessing of the input set, output prepocessing result and exit\n"

(*-------*)
let sub_typing_str = "--sub_typing"

let sub_typing_fun b =
  !current_options.sub_typing <- b

let sub_typing_inf =
  bool_str^
  inf_pref^"sub-type signature"

(*-------*)
let brand_transform_str = "--brand_transform"

let brand_transform_fun b =
  !current_options.brand_transform <- b

let brand_transform_inf =
  bool_str^
  inf_pref^"apply Brand's transformation to remove equality monotonicity axioms by flattening clauses\n"

(*-------*)
let min_unsat_core_str = "--min_unsat_core"

let min_unsat_core_fun b =
  !current_options.min_unsat_core <- b

let min_unsat_core_inf =
  bool_str^
  inf_pref^"minimise unsat core whenever is used; can be expenisve but can lead to shorter proofs and current state: for proofs better true for bmc1 better false \n"

(*-------Large Theories---------------*)

let large_theory_mode_str = "--large_theory_mode"

let large_theory_mode_fun b =
  !current_options.large_theory_mode <- b

let large_theory_mode_inf =
  bool_str^
  inf_pref^"Large theory mode\n"

(*--------*)

let prolific_symb_bound_str = "--prolific_symb_bound"

let prolific_symb_bound_fun int =
  !current_options.prolific_symb_bound <- int

let prolific_symb_bound_inf =
  int_str^
  inf_pref^"Large theory mode: if the number of occurrences of a symbol in the input is greater or equal to "^
  inf_pref^"prolific_symb_bound then the symbol is declared as prolific\n"

(*--------*)
let lt_threshold_str = "--lt_threshold"

let lt_threshold_fun int =
  !current_options.lt_threshold <- int

let lt_threshold_inf =
  int_str^
  inf_pref^"Large theory mode: if the number of input clauses >= threshold then the theory is considered to be large\n"^
  (dash_str "SAT Options")^"\n"

(*---Sat Mode-----*)
let sat_mode_str = "--sat_mode"

let sat_mode_fun b =
  !current_options.sat_mode <- b

let sat_mode_inf =
  bool_str^
  inf_pref^"Satisfiability mode \n"

(*--------*)
let sat_gr_def_str = "--sat_gr_def"

let sat_gr_def_fun b =
  !current_options.sat_gr_def <- b

let sat_gr_def_inf =
  bool_str^
  inf_pref^"Add definitions of ground terms in sat mode (!!do not use for now!!)\n"

(*--------*)
let sat_epr_types_str = "--sat_epr_types"

let sat_epr_types_fun b =
  !current_options.sat_epr_types <- b

let sat_epr_types_inf =
  bool_str^
  inf_pref^"using EPR types in sat mode\n"

(*--------*)
let sat_non_cyclic_types_str = "--sat_non_cyclic_types"

let sat_non_cyclic_types_fun b =
  !current_options.sat_non_cyclic_types <- b

let sat_non_cyclic_types_inf =
  bool_str^
  inf_pref^"using non cyclic types in sat mode\n"

(*--------*)
let sat_finite_models_str = "--sat_finite_models"

let sat_finite_models_fun b =
  !current_options.sat_finite_models <- b

let sat_finite_models_inf =
  bool_str^
  inf_pref^"Finite model finder, sat_mode should be true\n"

(*--------*)
let sat_out_model_str = "--sat_out_model"

let sat_out_model_fun str =
  try
    !current_options.sat_out_model <- str_to_sat_out_model_type str
  with
    Unknown_sat_model_out_type ->
      failwith (args_error_msg sat_out_model_str str)

let sat_out_model_inf =
  sat_out_model_type_str^
  inf_pref^"Outputs model if the input is shown satisfiable by instantiation. "^
  inf_pref^"Models are defined over ground terms (initial term algebra) "^
  inf_pref^"Predicates are defined as (\\forall x_1,..,x_n  ((~)P(x_1,..,x_n) <=> (\\phi(x_1,..,x_n)))) "^
  inf_pref^"where \\phi is a formula over the term algebra"^
  inf_pref^"If we have equality in the problem then it is also defined as a predicate above.\n"^
  inf_pref^"Using options we can output different models:"^
  inf_pref^"pos     -- using positive definitions (\\forall x_1,..,x_n  (P(x_1,..,x_n) <=> (\\phi(x_1,..,x_n))))"^
  inf_pref^"neg     -- using negative definitions (\\forall x_1,..,x_n  (~P(x_1,..,x_n) <=> (\\phi(x_1,..,x_n))))"^
  inf_pref^"small   -- choosing between positive and negative definitions according to the size "^
  inf_pref^"implied -- definitions of the form (\\forall x_1,..,x_n  ((~)P(x_1,..,x_n) <= (\\phi(x_1,..,x_n)))) "^
  inf_pref^"           if for some arguments a value of a predicate is not implied by these definitions "^
  inf_pref^"           then we can complete the model by choosing an arbitrary value of this predicate on these arguments"^
  inf_pref^"debug   -- in addition outputs 1) clauses with selected literals in the form {|L|;L_1;...;L_n}"^
  inf_pref^"           where |L| is the selected literal and 2) constraints"^
  inf_pref^"           Using debug it is possible to recover the justification of why each clause is true in the model\n"^
  inf_pref^"none     -- no model output \n"

(*--------*)
let sat_out_clauses_str = "--sat_out_clauses"

let sat_out_clauses_fun b =
  !current_options.sat_out_clauses <- b

let sat_out_clauses_inf =
  bool_str^
  inf_pref^"Outputs all active clauses if the input is show satisfiable. "^
  (* ugly hack *)
  (dash_str "BMC1 Options")^"\n"

(*----BMC1---------------*)

let bmc1_incremental_str = "--bmc1_incremental"

let bmc1_incremental_fun b =
  !current_options.bmc1_incremental <-
    override_cmd b !current_options.bmc1_incremental

let bmc1_incremental_inf =
  bool_str^
  inf_pref^"incrementally increase bounds in BMC1\n"

(*--------*)

let bmc1_axioms_str = "--bmc1_axioms"

let bmc1_axioms_fun str =
  try
    !current_options.bmc1_axioms <-
      (override_cmd
	 (str_to_bmc1_axioms_type str)
	 !current_options.bmc1_axioms)
  with
    Unknown_bmc1_axioms_type ->
      failwith (args_error_msg bmc1_axioms_str str)

let bmc1_axioms_inf =
  bmc1_axioms_type_list_str^
  inf_pref^"axioms for BMC1\n"

(*--------*)

let bmc1_min_bound_str = "--bmc1_min_bound"

let bmc1_min_bound_fun b =
  !current_options.bmc1_min_bound <-
    override_cmd b !current_options.bmc1_min_bound

let bmc1_min_bound_inf =
  int_str^
  inf_pref^"starting bound in BMC1\n"

(*--------*)

let bmc1_max_bound_str = "--bmc1_max_bound"

let bmc1_max_bound_fun b =
  !current_options.bmc1_max_bound <-
    override_cmd b !current_options.bmc1_max_bound

let bmc1_max_bound_inf =
  int_str^
  inf_pref^"maximal bound in BMC1, -1 for unlimited\n"

(*--------*)

let bmc1_max_bound_default_str = "--bmc1_max_bound_default"

let bmc1_max_bound_default_fun b =
  !current_options.bmc1_max_bound_default <-
    override_cmd b !current_options.bmc1_max_bound_default

let bmc1_max_bound_default_inf =
  int_str^
  inf_pref^"maximal bound in BMC1 unless higher bound from file\n"

(*--------*)

let bmc1_symbol_reachability_str = "--bmc1_symbol_reachability"

let bmc1_symbol_reachability_fun b =
  !current_options.bmc1_symbol_reachability <- b

let bmc1_symbol_reachability_inf =
  bool_str^
  inf_pref^"calculate symbol reachability for father/son relation in Intel BMC1; \n"

(*--------*)

let bmc1_add_unsat_core_str = "--bmc1_add_unsat_core"

let bmc1_add_unsat_core_fun str =
  try
    !current_options.bmc1_add_unsat_core <-
      override_cmd
	(str_to_bmc1_add_unsat_core_type str)
	!current_options.bmc1_add_unsat_core
  with
    Unknown_bmc1_add_unsat_core_type ->
      failwith (args_error_msg bmc1_add_unsat_core_str str)

let bmc1_add_unsat_core_inf =
  bmc1_add_unsat_core_type_list_str^
  inf_pref^"add clauses in unsatisfiable core to next bound in BMC1\n"

(*--------*)

let bmc1_unsat_core_children_str = "--bmc1_unsat_core_children"

let bmc1_unsat_core_children_fun b =
  !current_options.bmc1_unsat_core_children <-
    override_cmd b !current_options.bmc1_unsat_core_children

let bmc1_unsat_core_children_inf =
  bool_str^
  inf_pref^"children of unsat core clauses are considered in unsat core\n"

(*--------*)

let bmc1_unsat_core_extrapolate_axioms_str =
  "--bmc1_unsat_core_extrapolate_axioms"

let bmc1_unsat_core_extrapolate_axioms_fun b =
  !current_options.bmc1_unsat_core_extrapolate_axioms <-
    override_cmd b !current_options.bmc1_unsat_core_extrapolate_axioms

let bmc1_unsat_core_extrapolate_axioms_inf =
  bool_str^
  inf_pref^"extrapolate axioms to next bound in unsat core\n"

(*--------*)

let bmc1_out_stat_str = "--bmc1_out_stat"

let bmc1_out_stat_fun str =
  try
    !current_options.bmc1_out_stat <-
      (override_cmd
	 (str_to_bmc1_out_stat_type str)
	 !current_options.bmc1_out_stat)
  with
    Unknown_bmc1_out_stat_type ->
      failwith (args_error_msg bmc1_out_stat_str str)

let bmc1_out_stat_inf =
  bmc1_out_stat_type_list_str^
  inf_pref^"output no statistics, after the last bound only or after each bound (full)\n"

(*--------*)
let bmc1_pre_inst_next_state_str = "--bmc1_pre_inst_next_state"

let bmc1_pre_inst_next_state_fun b =
  !current_options.bmc1_pre_inst_next_state <- b

let bmc1_pre_inst_next_state_inf =
  bool_str^
  inf_pref^"pre-instantiate $$nextState(x,y) -> phi(x,y) axioms \n"

(*--------*)
let bmc1_pre_inst_state_str = "--bmc1_pre_inst_state"

let bmc1_pre_inst_state_fun b =
  !current_options.bmc1_pre_inst_state <- b

let bmc1_pre_inst_state_inf =
  bool_str^
  inf_pref^"pre-instantiate clauses with state variables by the current bound; \n"^
  inf_pref^"if \"--bmc1_pre_inst_state true\" then it  should be --bmc1_pre_inst_next_state true and --bmc1_pre_inst_reach_state true\n"

(*--------*)
let bmc1_pre_inst_reach_state_str = "--bmc1_pre_inst_reach_state"

let bmc1_pre_inst_reach_state_fun b =
  !current_options.bmc1_pre_inst_reach_state <- b

let bmc1_pre_inst_reach_state_inf =
  bool_str^
  inf_pref^"pre-instantiate $$reachableState(X) -> X = $$constB0 \\/...\\/X=$$constBn axioms \n"

(*--------*)

let bmc1_out_unsat_core_str = "--bmc1_out_unsat_core"

let bmc1_out_unsat_core_fun b =
  !current_options.bmc1_out_unsat_core <-
    override_cmd b !current_options.bmc1_out_unsat_core

let bmc1_out_unsat_core_inf =
  bool_str^
  inf_pref^"output unsat core for each bound in BMC1\n"

(*--------*)

let bmc1_dump_clauses_tptp_str = "--bmc1_dump_clauses_tptp"

let bmc1_dump_clauses_tptp_fun b =
  !current_options.bmc1_dump_clauses_tptp <-
    override_cmd b !current_options.bmc1_dump_clauses_tptp

let bmc1_dump_clauses_tptp_inf =
  bool_str^
  inf_pref^"dump clauses for each bound in BMC1 in TPTP format\n"

(*--------*)

let bmc1_dump_unsat_core_tptp_str = "--bmc1_dump_unsat_core_tptp"

let bmc1_dump_unsat_core_tptp_fun b =
  !current_options.bmc1_dump_unsat_core_tptp <-
    override_cmd b !current_options.bmc1_dump_unsat_core_tptp

let bmc1_dump_unsat_core_tptp_inf =
  bool_str^
  inf_pref^"dump unsat core for each bound in BMC1 in TPTP format\n"

(*--------*)

let bmc1_dump_file_str = "--bmc1_dump_file"

let bmc1_dump_file_fun b =
  !current_options.bmc1_dump_file <-
    override_cmd (Some b) !current_options.bmc1_dump_file

let bmc1_dump_file_inf =
  bool_str^
  inf_pref^"file to write clauses into\n"

(*--------*)

let bmc1_verbose_str = "--bmc1_verbose"

let bmc1_verbose_fun b =
  !current_options.bmc1_verbose <-
    override_cmd b !current_options.bmc1_verbose

let bmc1_verbose_inf =
  bool_str^
  inf_pref^"print detailed output during incremental BMC1\n" ^
  (* ugly hack *)
  (dash_str "Instantiation Options")^"\n"

(*----Instantiation------*)

let instantiation_flag_str = "--instantiation_flag"

let instantiation_flag_fun b =
  !current_options.instantiation_flag <- b

let instantiation_flag_inf =
  bool_str^
  inf_pref^"switches instantiation on/off\n"

(*--------*)

let inst_lit_sel_str = "--inst_lit_sel"

let inst_lit_sel_fun str =
  try
    let str_list = parse_list_opt str in
    let inst_lit_sel = List.map str_to_lit_cmp_type str_list in
    !current_options.inst_lit_sel <- inst_lit_sel
  with
  | Parse_list_fail | Unknown_lit_cmp_type ->
      failwith (args_error_msg inst_lit_sel_str str)

let inst_lit_sel_inf =
  lit_cmp_type_list_str^
  inf_pref^"instantiation selection function is a lex product of functions in the list"^
  example_str^inst_lit_sel_str^" [+sign;+ground;-num_symb]"^
  inf_pref^"in this ex. priority is given to positive literals,"^
  inf_pref^"then to ground and then to lits with fewer number of symbols\n"

(*--------*)
let inst_solver_per_active_str = "--inst_solver_per_active"

let inst_solver_per_active_fun i =
  !current_options.inst_solver_per_active <- i

let inst_solver_per_active_inf =
  int_str^
  inf_pref^"number of propositional solver calls per active clauses\n"

(*--------*)

let inst_solver_per_clauses_str = "--inst_solver_per_clauses"

let inst_solver_per_clauses_fun i =
  !current_options.inst_solver_per_clauses <- i

let inst_solver_per_clauses_inf =
  int_str^
  inf_pref^"number of propositional solver calls per generated clauses\n"

(*--------*)

let inst_pass_queue1_str = "--inst_pass_queue1"

let inst_pass_queue1_fun str =
  try
    let str_list = parse_list_opt str in
    let queue = List.map str_to_cl_cmp_type str_list in
    
    !current_options.inst_pass_queue1 <-
      override_cmd queue !current_options.inst_pass_queue1
	
  with
  | Parse_list_fail | Unknown_cl_cmp_type ->
      failwith (args_error_msg inst_pass_queue1_str str)

let inst_pass_queue1_inf =
  cl_cmp_type_list_str^
  inf_pref^"first passive priority queue for instantiation "^
  inf_pref^"priority is based on lex combination of parameters in the list"^
  example_str^inst_pass_queue1_str^" [-num_var;-num_symb]"^
  inf_pref^"in this ex. priority is given to clauses with fewer number of vars"^
  inf_pref^"then with fewer number of symbols\n"

(*--------*)

let inst_pass_queue2_str = "--inst_pass_queue2"

let inst_pass_queue2_fun str =
  try
    let str_list = parse_list_opt str in
    let queue = List.map str_to_cl_cmp_type str_list in
    
    !current_options.inst_pass_queue2 <-
      override_cmd queue !current_options.inst_pass_queue2
	
  with
  | Parse_list_fail | Unknown_cl_cmp_type ->
      failwith (args_error_msg inst_pass_queue2_str str)

let inst_pass_queue2_inf =
  cl_cmp_type_list_str^
  inf_pref^"second passive priority queue for instantiation "^
  inf_pref^"priority is based on lex combination of parameters in the list"^
  example_str^inst_pass_queue2_str^" [+age;-num_symb]"^
  inf_pref^"in this ex. priority is given to clauses which were generated at an earlier stage"^
  inf_pref^"then with fewer number of symbols\n"

(*--------*)

let inst_pass_queue3_str = "--inst_pass_queue3"

let inst_pass_queue3_fun str =
  try
    let str_list = parse_list_opt str in
    let queue = List.map str_to_cl_cmp_type str_list in
    
    !current_options.inst_pass_queue3 <-
      override_cmd queue !current_options.inst_pass_queue3
	
  with
  | Parse_list_fail | Unknown_cl_cmp_type ->
      failwith (args_error_msg inst_pass_queue3_str str)

let inst_pass_queue3_inf =
  cl_cmp_type_list_str^
  inf_pref^"third passive priority queue for instantiation "^
  inf_pref^"priority is based on lex combination of parameters in the list"^
  example_str^inst_pass_queue3_str^" [+age;-num_symb]"^
  inf_pref^"in this ex. priority is given to clauses which were generated at an earlier stage"^
  inf_pref^"then with fewer number of symbols\n"

(*--------*)

let inst_pass_queue1_mult_str = "--inst_pass_queue1_mult"

let inst_pass_queue1_mult_fun i =
  
  !current_options.inst_pass_queue1_mult <-
    override_cmd i !current_options.inst_pass_queue1_mult

let inst_pass_queue1_mult_inf =
  int_str^
  inf_pref^"first priority queue multiple:"^
  inf_pref^"the number of clauses taken before switching to the next queue\n"

(*--------*)

let inst_pass_queue2_mult_str = "--inst_pass_queue2_mult"

let inst_pass_queue2_mult_fun i =
  
  !current_options.inst_pass_queue2_mult <-
    override_cmd i !current_options.inst_pass_queue2_mult

let inst_pass_queue2_mult_inf =
  int_str^
  inf_pref^"second priority queue multiple:"^
  inf_pref^"the number of clauses taken before switching to the next queue\n"

(*--------*)

let inst_pass_queue3_mult_str = "--inst_pass_queue3_mult"

let inst_pass_queue3_mult_fun i =
  
  !current_options.inst_pass_queue3_mult <-
    override_cmd i !current_options.inst_pass_queue3_mult

let inst_pass_queue3_mult_inf =
  int_str^
  inf_pref^"third priority queue multiple:"^
  inf_pref^"the number of clauses taken before switching to the next queue\n"

(*--------*)

let inst_dismatching_str = "--inst_dismatching"

let inst_dismatching_fun b =
  !current_options.inst_dismatching <- b

let inst_dismatching_inf =
  bool_str^
  inf_pref^"Dismatching constraints for instantiation\n"

(*--------*)

let inst_eager_unprocessed_to_passive_str = "--inst_eager_unprocessed_to_passive"

let inst_eager_unprocessed_to_passive_fun b =
  !current_options.inst_eager_unprocessed_to_passive <- b

let inst_eager_unprocessed_to_passive_inf =
  bool_str^"\n"

(*--------*)

let inst_prop_sim_given_str = "--inst_prop_sim_given"

let inst_prop_sim_given_fun b =
  !current_options.inst_prop_sim_given <- b

let inst_prop_sim_given_inf =
  bool_str^
  inf_pref^"instantiation: propositional simplification of the given clause\n"

(*--------*)

let inst_prop_sim_new_str = "--inst_prop_sim_new"

let inst_prop_sim_new_fun b =
  !current_options.inst_prop_sim_new <- b

let inst_prop_sim_new_inf =
  bool_str^
  inf_pref^"instantiation: propositional simplification of newly produced clauses\n"

(*--------*)

let inst_orphan_elimination_str = "--inst_orphan_elimination"

let inst_orphan_elimination_fun b = 
  !current_options.inst_orphan_elimination <- b 

let inst_orphan_elimination_inf = 
  bool_str^
  inf_pref^"eliminates children if the parent gets eliminated; here only children obtained by instantiation are considered\n"


(*--------*)

let inst_learning_loop_flag_str = "--inst_learning_loop_flag"

let inst_learning_loop_flag_fun b =
  !current_options.inst_learning_loop_flag <- b

let inst_learning_loop_flag_inf =
  bool_str^
  inf_pref^"simple learning: restart instantiation after"^
  inf_pref^"inst_learning_start inst. loop iterations"^
  inf_pref^"keeping propositional set of clauses"^
  inf_pref^"which provides better guided proof search\n"

(*--------*)
let inst_learning_start_str = "--inst_learning_start"

let inst_learning_start_fun i =
  !current_options.inst_learning_start <- i

let inst_learning_start_inf =
  int_str^
  inf_pref^"number of instantiation loops before learning starts\n"

(*--------*)
let inst_learning_factor_str = "--inst_learning_factor"

let inst_learning_factor_fun i =
  !current_options.inst_learning_factor <- i

let inst_learning_factor_inf =
  int_str^
  inf_pref^"learning is repeated after that"^
  inf_pref^"the bound on number of loops is multiplied by this factor\n"

(*--------*)
let inst_start_prop_sim_after_learn_str = "--inst_start_prop_sim_after_learn"

let inst_start_prop_sim_after_learn_fun i =
  !current_options.inst_start_prop_sim_after_learn <- i

let inst_start_prop_sim_after_learn_inf =
  int_str^
  inf_pref^"prop simplification starts after"^
  inf_pref^"inst_start_prop_sim_after_learn of learning restarts\n"

(*--------*)

let inst_sel_renew_str = "--inst_sel_renew"

let inst_sel_renew_fun str =
  try
    !current_options.inst_sel_renew <- (str_to_inst_sel_renew_type str)
  with
    Unknown_out_options_type ->
      failwith (args_error_msg inst_sel_renew_str str)

let inst_sel_renew_inf =
  "<model|solver>"^
  inf_pref^" Selection is either based on (i) pre stored model and model values are tried to be enforced, or"^
  inf_pref^" (ii) current sat solver values \n"

(*--------*)

let inst_lit_activity_flag_str = "--inst_lit_activity_flag"

let inst_lit_activity_flag_fun b =
  !current_options.inst_lit_activity_flag <- b

let inst_lit_activity_flag_inf =
  bool_str^
  inf_pref^"if true then overactive literals are tried to be deselected in propositional models\n"

(*--------*)

let inst_out_proof_str = "--inst_out_proof"

let inst_out_proof_fun b =
  !current_options.inst_out_proof <-
    override_cmd b !current_options.inst_out_proof

let inst_out_proof_inf =
  bool_str^
  inf_pref^"output proofs from instantiation\n"^
  (* ugly hack *)
  (dash_str "Resolution Options")^"\n"

(*----Resolution------*)

let resolution_flag_str = "--resolution_flag"

let resolution_flag_fun b =
  !current_options.resolution_flag <- b

let resolution_flag_inf =
  bool_str^
  inf_pref^"switches resolution on/off\n"

(*--------*)

let res_lit_sel_str = "--res_lit_sel"

let res_lit_sel_fun str =
  try
    !current_options.res_lit_sel <- (str_to_sel_type str)
  with
    Unknown_res_sel_fun_type ->
      failwith (args_error_msg res_lit_sel_str str)

let res_lit_sel_inf =
  "<adaptive|kbo_max|neg_max|neg_min>"^
  inf_pref^"resolution literal selection functions:"^
  inf_pref^"adaptive: select negative literals until no inference possible"^
  inf_pref^"          then change to kbo maximal"^
  inf_pref^"kbo_max: select kbo maximal literals"^
  inf_pref^"neg_max: select negative literals with a maximal number of symbols, otherwise kbo_max"^
  inf_pref^"neg_min: select negative literals with a minimal number of symbols, otherwise kbo_max\n"

(*--------*)
let res_to_prop_solver_str = "--res_to_prop_solver"

let res_to_prop_solver_fun str =
  try
    !current_options.res_to_prop_solver <- (str_to_res_to_prop_solver_type str)
  with
    Unknown_res_to_prop_solver_type ->
      failwith (args_error_msg res_to_prop_solver_str str)

let res_to_prop_solver_inf =
  "<active | passive | none>"^
  inf_pref^"adding grounding of clauses to the propositional solver\n"

(*--------*)
let res_prop_simpl_new_str = "--res_prop_simpl_new"

let res_prop_simpl_new_fun b =
  !current_options.res_prop_simpl_new <- b

let res_prop_simpl_new_inf =
  bool_str^
  inf_pref^"propositionally simplify newly generated (by resolution) clauses\n"

(*--------*)
let res_prop_simpl_given_str = "--res_prop_simpl_given"

let res_prop_simpl_given_fun b =
  !current_options.res_prop_simpl_given <- b

let res_prop_simpl_given_inf =
  bool_str^
  inf_pref^"propositionally simplify given (in the resolution loop) clauses\n"

(*--------*)
let res_passive_queue_flag_str = "--res_passive_queue_flag"

let res_passive_queue_flag_fun b =
  !current_options.res_passive_queue_flag <- b

let res_passive_queue_flag_inf =
  bool_str^
  inf_pref^"if true then passive priority queues else simple queue is used\n"

(*--------*)

let res_pass_queue1_str = "--res_pass_queue1"

let res_pass_queue1_fun str =
  try
    let str_list = parse_list_opt str in
    let queue = List.map str_to_cl_cmp_type str_list in
    !current_options.res_pass_queue1 <- queue
  with
  | Parse_list_fail | Unknown_cl_cmp_type ->
      failwith (args_error_msg res_pass_queue1_str str)

let res_pass_queue1_inf =
  cl_cmp_type_list_str^
  inf_pref^"first passive priority queue for resolution "^
  inf_pref^"priority is based on lex combination of parameters in the list"^
  example_str^res_pass_queue1_str^" [-num_var;-num_symb]"^
  inf_pref^"in this ex. priority is given to clauses with fewer number of vars"^
  inf_pref^"then with fewer number of symbols\n"

(*--------*)

let res_pass_queue2_str = "--res_pass_queue2"

let res_pass_queue2_fun str =
  try
    let str_list = parse_list_opt str in
    let queue = List.map str_to_cl_cmp_type str_list in
    !current_options.res_pass_queue2 <- queue
  with
  | Parse_list_fail | Unknown_cl_cmp_type ->
      failwith (args_error_msg res_pass_queue2_str str)

let res_pass_queue2_inf =
  cl_cmp_type_list_str^
  inf_pref^"second passive priority queue for resolution "^
  inf_pref^"priority is based on lex combination of parameters in the list"^
  example_str^res_pass_queue2_str^" [+age;-num_symb]"^
  inf_pref^"in this ex. priority is given to clauses which were generated at an earlier stage"^
  inf_pref^"then with fewer number of symbols\n"

(*--------*)

let res_pass_queue1_mult_str = "--res_pass_queue1_mult"

let res_pass_queue1_mult_fun i =
  !current_options.res_pass_queue1_mult <- i

let res_pass_queue1_mult_inf =
  int_str^
  inf_pref^"first priority queue multiple:"^
  inf_pref^"the number of clauses taken before switching to the next queue\n"

(*--------*)

let res_pass_queue2_mult_str = "--res_pass_queue2_mult"

let res_pass_queue2_mult_fun i =
  !current_options.res_pass_queue2_mult <- i

let res_pass_queue2_mult_inf =
  int_str^
  inf_pref^"second priority queue multiple:"^
  inf_pref^"the number of clauses taken before switching to the next queue\n"

(*--------*)
let res_forward_subs_str = "--res_forward_subs"

let res_forward_subs_fun str =
  try
    !current_options.res_forward_subs <- (str_to_res_subs_type str)
  with Unknown_res_subs_type ->
    failwith (args_error_msg res_forward_subs_str str)

let res_forward_subs_inf =
  res_subs_type_str^
  inf_pref^"full:                 full forward subsumption"^
  inf_pref^"subset_subsumption:   efficient but incomplete (always on);"^
  inf_pref^"length[n]:            subsumption by clauses of length less or equal to n"^
  example_str^res_forward_subs_str^" length[1]\n"

(*--------*)

let res_backward_subs_str = "--res_backward_subs"

let res_backward_subs_fun str =
  try
    !current_options.res_backward_subs <- (str_to_res_subs_type str)
  with Unknown_res_subs_type ->
    failwith (args_error_msg res_backward_subs_str str)

let res_backward_subs_inf =
  res_subs_type_str^
  inf_pref^"full:                 full forward subsumption"^
  inf_pref^"subset_subsumption:   efficient but incomplete (always on);"^
  inf_pref^"length[n]:            subsumption by clauses of length less or equal to n"^
  example_str^res_backward_subs_str^" length[1]\n"

(*--------*)

let res_forward_subs_resolution_str = "--res_forward_subs_resolution"

let res_forward_subs_resolution_fun b =
  !current_options.res_forward_subs_resolution <- b

let res_forward_subs_resolution_inf =
  bool_str^
  inf_pref^"forward subsumption resolution\n"

(*--------*)
let res_backward_subs_resolution_str = "--res_backward_subs_resolution"

let res_backward_subs_resolution_fun b =
  !current_options.res_backward_subs_resolution <- b

let res_backward_subs_resolution_inf =
  bool_str^
  inf_pref^"backward subsumption resolution\n"

(*--------*)
let res_orphan_elimination_str = "--res_orphan_elimination"

let res_orphan_elimination_fun b =
  !current_options.res_orphan_elimination <- b

let res_orphan_elimination_inf =
  bool_str^
  inf_pref^"orphan elimination\n"

(*--------*)
let res_time_limit_str = "--res_time_limit"

let res_time_limit_fun f =
  !current_options.res_time_limit <- f

let res_time_limit_inf =
  float_str^
  inf_pref^"time limit (in seconds) for each iteration of the resolution loop\n"

(*--------*)
let res_out_proof_str = "--res_out_proof"

let res_out_proof_fun b =
  !current_options.res_out_proof <- b

let res_out_proof_inf =
  bool_str^
  inf_pref^"Outputs the proof, if it is found by resolution\n"^
  (* ugly hack *)
  (dash_str "Combination Options")^"\n"

(*----Combination--------*)

let comb_res_mult_str = "--comb_res_mult"

let comb_res_mult_fun i =
  !current_options.comb_res_mult <- i

let comb_res_mult_inf =
  int_str^
  inf_pref^"resolution multiple in combination of instantiation and resolution\n"

(*--------*)
let comb_inst_mult_str = "--comb_inst_mult"

let comb_inst_mult_fun i =
  !current_options.comb_inst_mult <- i

let comb_inst_mult_inf =
  int_str^
  inf_pref^"instantiation multiple in combination of instantiation and resolution\n"^
  (* ugly hack *)
  (dash_str "Remaining Options")^"\n"

(*

  let _str = "--"

  let _fun =
  !current_options. <-

  let _inf =
  ^
  inf_pref^

  inf_pref^
  inf_pref^

  !current_options
  !current_options.
  !current_options.
  !current_options.
 *)

(*let info_str str = "\n    "^str*)
let spec_list =
  [(out_options_str, Arg.String(out_options_fun), out_options_inf);
   (tptp_safe_out_str, Arg.Bool(tptp_safe_out_fun), tptp_safe_out_inf);
   (problem_path_str, Arg.String(problem_path_fun), problem_path_inf);
   (include_path_str, Arg.String(include_path_fun), include_path_inf);
   (clausifier_str, Arg.String(clausifier_fun), clausifier_inf);
   (clausifier_options_str, Arg.String(clausifier_options_fun), clausifier_options_inf);
   (stdin_str, Arg.Bool(stdin_fun), stdin_inf);
   (dbg_backtrace_str, Arg.Bool(dbg_backtrace_fun), dbg_backtrace_inf);
   (dbg_dump_prop_clauses_str,
    Arg.Bool(dbg_dump_prop_clauses_fun),
    dbg_dump_prop_clauses_inf);
   (dbg_dump_prop_clauses_file_str,
    Arg.String(dbg_dump_prop_clauses_file_fun),
    dbg_dump_prop_clauses_file_inf);
   (dbg_out_stat_str, Arg.Bool(dbg_out_stat_fun), dbg_out_stat_inf);
   
   (*------General-------*)
   (fof_str, Arg.Bool(fof_fun), fof_inf);
   (time_out_real_str, Arg.Float(time_out_real_fun), time_out_real_inf);
   (time_out_virtual_str, Arg.Float(time_out_virtual_fun), time_out_virtual_inf);
   (schedule_str, Arg.String(schedule_fun), schedule_inf);
   (ground_splitting_str, Arg.String(ground_splitting_fun), ground_splitting_inf);
   (non_eq_to_eq_str, Arg.Bool(non_eq_to_eq_fun), non_eq_to_eq_inf);
   (prep_gs_sim_str, Arg.Bool(prep_gs_sim_fun), prep_gs_sim_inf);
   (prep_res_sim_str, Arg.Bool(prep_res_sim_fun), prep_res_sim_inf);
   (res_sim_input_str, Arg.Bool(res_sim_input_fun), res_sim_input_inf);
   (clause_weak_htbl_str, Arg.Bool(clause_weak_htbl_fun), clause_weak_htbl_inf);
   (gc_record_bc_elim_str, Arg.Bool(gc_record_bc_elim_fun), gc_record_bc_elim_inf);
   (symbol_type_check_str, Arg.Bool(symbol_type_check_fun), symbol_type_check_inf);
   (clausify_out_str, Arg.Bool(clausify_out_fun), clausify_out_inf);
   (prep_sem_filter_str, Arg.String(prep_sem_filter_fun), prep_sem_filter_inf);
   (prep_sem_filter_out_str, Arg.Bool(prep_sem_filter_out_fun), prep_sem_filter_out_inf);
   (sub_typing_str, Arg.Bool(sub_typing_fun), sub_typing_inf);
   (brand_transform_str, Arg.Bool(brand_transform_fun), brand_transform_inf);
   (min_unsat_core_str, Arg.Bool(min_unsat_core_fun), min_unsat_core_inf);
   
   (*---Large Theories----*)
   (large_theory_mode_str, Arg.Bool(large_theory_mode_fun), large_theory_mode_inf);
   
   (prolific_symb_bound_str, Arg.Int(prolific_symb_bound_fun), prolific_symb_bound_inf);
   (lt_threshold_str, Arg.Int(lt_threshold_fun), lt_threshold_inf);
   
   (*-----Sat Mode----------*)
   (sat_mode_str, Arg.Bool(sat_mode_fun), sat_mode_inf);
   (sat_gr_def_str, Arg.Bool(sat_gr_def_fun), sat_gr_def_inf);
   (sat_epr_types_str, Arg.Bool(sat_epr_types_fun), sat_epr_types_inf);
   (sat_non_cyclic_types_str, Arg.Bool(sat_non_cyclic_types_fun), sat_non_cyclic_types_inf);
   (sat_finite_models_str, Arg.Bool(sat_finite_models_fun), sat_finite_models_inf);
   (sat_out_model_str, Arg.String(sat_out_model_fun), sat_out_model_inf);
   (sat_out_clauses_str, Arg.Bool(sat_out_clauses_fun), sat_out_clauses_inf);
   
   (*----BMC1---------------*)
   (bmc1_incremental_str,
    Arg.Bool(bmc1_incremental_fun),
    bmc1_incremental_inf);
   
   (bmc1_axioms_str,
    Arg.String(bmc1_axioms_fun),
    bmc1_axioms_inf);
   
   (bmc1_min_bound_str,
    Arg.Int(bmc1_min_bound_fun),
    bmc1_min_bound_inf);
   
   (bmc1_max_bound_str,
    Arg.Int(bmc1_max_bound_fun),
    bmc1_max_bound_inf);
   
   (bmc1_max_bound_default_str,
    Arg.Int(bmc1_max_bound_default_fun),
    bmc1_max_bound_default_inf);
   
   (bmc1_symbol_reachability_str,
    Arg.Bool(bmc1_symbol_reachability_fun),
    bmc1_symbol_reachability_inf);
   
   (bmc1_add_unsat_core_str,
    Arg.String(bmc1_add_unsat_core_fun),
    bmc1_add_unsat_core_inf);
   
   (bmc1_unsat_core_children_str,
    Arg.Bool(bmc1_unsat_core_children_fun),
    bmc1_unsat_core_children_inf);
   
   (bmc1_unsat_core_extrapolate_axioms_str,
    Arg.Bool(bmc1_unsat_core_extrapolate_axioms_fun),
    bmc1_unsat_core_extrapolate_axioms_inf);
   
   (bmc1_out_stat_str,
    Arg.String(bmc1_out_stat_fun),
    bmc1_out_stat_inf);
   
   (bmc1_pre_inst_next_state_str,
    Arg.Bool(bmc1_pre_inst_next_state_fun),
    bmc1_pre_inst_next_state_inf);
   
   (bmc1_pre_inst_state_str,
    Arg.Bool(bmc1_pre_inst_state_fun),
    bmc1_pre_inst_state_inf);
   
   (bmc1_pre_inst_reach_state_str,
    Arg.Bool(bmc1_pre_inst_reach_state_fun),
    bmc1_pre_inst_reach_state_inf);
   
   (bmc1_out_unsat_core_str,
    Arg.Bool(bmc1_out_unsat_core_fun),
    bmc1_out_unsat_core_inf);
   
   (bmc1_dump_clauses_tptp_str,
    Arg.Bool(bmc1_dump_clauses_tptp_fun),
    bmc1_dump_clauses_tptp_inf);
   
   (bmc1_dump_unsat_core_tptp_str,
    Arg.Bool(bmc1_dump_unsat_core_tptp_fun),
    bmc1_dump_unsat_core_tptp_inf);
   
   (bmc1_dump_file_str,
    Arg.String(bmc1_dump_file_fun),
    bmc1_dump_file_inf);
   
   (bmc1_verbose_str,
    Arg.Bool(bmc1_verbose_fun),
    bmc1_verbose_inf);
   
   (*------Instantiation--*)
   (instantiation_flag_str, Arg.Bool(instantiation_flag_fun), instantiation_flag_inf);
   (inst_lit_sel_str, Arg.String(inst_lit_sel_fun), inst_lit_sel_inf);
   (inst_solver_per_active_str,
    Arg.Int(inst_solver_per_active_fun), inst_solver_per_active_inf);
   (inst_solver_per_clauses_str,
    Arg.Int(inst_solver_per_clauses_fun), inst_solver_per_clauses_inf);
   (inst_pass_queue1_str,
    Arg.String(inst_pass_queue1_fun), inst_pass_queue1_inf);
   (inst_pass_queue2_str,
    Arg.String(inst_pass_queue2_fun), inst_pass_queue2_inf);
   (inst_pass_queue3_str,
    Arg.String(inst_pass_queue3_fun), inst_pass_queue3_inf);
   (inst_pass_queue1_mult_str,
    Arg.Int(inst_pass_queue1_mult_fun), inst_pass_queue1_mult_inf);
   (inst_pass_queue2_mult_str,
    Arg.Int(inst_pass_queue2_mult_fun), inst_pass_queue2_mult_inf);
   (inst_pass_queue3_mult_str,
    Arg.Int(inst_pass_queue3_mult_fun), inst_pass_queue3_mult_inf);
   (inst_dismatching_str, Arg.Bool(inst_dismatching_fun), inst_dismatching_inf);
   (inst_eager_unprocessed_to_passive_str,
    Arg.Bool(inst_eager_unprocessed_to_passive_fun),
    inst_eager_unprocessed_to_passive_inf);
   (inst_prop_sim_given_str,
    Arg.Bool(inst_prop_sim_given_fun), inst_prop_sim_given_inf);
   (inst_prop_sim_new_str, Arg.Bool(inst_prop_sim_new_fun), inst_prop_sim_new_inf);
   (inst_orphan_elimination_str, Arg.Bool(inst_orphan_elimination_fun), inst_orphan_elimination_inf);
   (inst_learning_loop_flag_str,
    Arg.Bool(inst_learning_loop_flag_fun), inst_learning_loop_flag_inf);
   (inst_learning_start_str,
    Arg.Int(inst_learning_start_fun), inst_learning_start_inf);
   (inst_learning_factor_str,
    Arg.Int(inst_learning_factor_fun), inst_learning_factor_inf);
   (inst_start_prop_sim_after_learn_str,
    Arg.Int(inst_start_prop_sim_after_learn_fun), inst_start_prop_sim_after_learn_inf);
   (inst_sel_renew_str, Arg.String(inst_sel_renew_fun), inst_sel_renew_inf);
   (inst_lit_activity_flag_str, Arg.Bool(inst_lit_activity_flag_fun), inst_lit_activity_flag_inf);
   (inst_out_proof_str, Arg.Bool(inst_out_proof_fun), inst_out_proof_inf);
   
   (*------Resolution--*)
   (resolution_flag_str, Arg.Bool(resolution_flag_fun), resolution_flag_inf);
   (res_lit_sel_str, Arg.String(res_lit_sel_fun), res_lit_sel_inf);
   (res_to_prop_solver_str, Arg.String(res_to_prop_solver_fun), res_to_prop_solver_inf);
   (res_prop_simpl_new_str,
    Arg.Bool(res_prop_simpl_new_fun), res_prop_simpl_new_inf);
   (res_prop_simpl_given_str,
    Arg.Bool(res_prop_simpl_given_fun), res_prop_simpl_given_inf);
   (res_passive_queue_flag_str,
    Arg.Bool(res_passive_queue_flag_fun), res_passive_queue_flag_inf);
   (res_pass_queue1_str, Arg.String(res_pass_queue1_fun), res_pass_queue1_inf);
   (res_pass_queue2_str, Arg.String(res_pass_queue2_fun), res_pass_queue2_inf);
   (res_pass_queue1_mult_str,
    Arg.Int(res_pass_queue1_mult_fun), res_pass_queue1_mult_inf);
   (res_pass_queue2_mult_str,
    Arg.Int(res_pass_queue2_mult_fun), res_pass_queue2_mult_inf);
   (res_forward_subs_str,
    Arg.String(res_forward_subs_fun), res_forward_subs_inf);
   (res_backward_subs_str,
    Arg.String(res_backward_subs_fun), res_backward_subs_inf);
   (res_forward_subs_resolution_str,
    Arg.Bool(res_forward_subs_resolution_fun), res_forward_subs_resolution_inf);
   (res_backward_subs_resolution_str,
    Arg.Bool(res_backward_subs_resolution_fun), res_backward_subs_resolution_inf);
   (res_orphan_elimination_str,
    Arg.Bool(res_orphan_elimination_fun), res_orphan_elimination_inf);
   (res_time_limit_str, Arg.Float(res_time_limit_fun), res_time_limit_inf);
   (res_out_proof_str, Arg.Bool(res_out_proof_fun), res_out_proof_inf);
   (comb_res_mult_str, Arg.Int(comb_res_mult_fun), comb_res_mult_inf);
   (comb_inst_mult_str, Arg.Int(comb_inst_mult_fun), comb_inst_mult_inf);
   (*
     (_str, Arg.(_fun), _inf);
    *)
 ]

(*--------Options output-----------------*)

type opt_val_type = string * string

let val_distance = 40

let opt_val_to_str opt_val =
  let (opt_name, val_str') = opt_val in
  let tptp_safe_opt_name = tptp_safe_str opt_name in
  let val_str =
    if val_str' = "" then "\"\"" else val_str' in
  (space_padding_str val_distance tptp_safe_opt_name)^val_str

let opt_val_list_to_str l =
  String.concat "\n" (List.map opt_val_to_str l)

let input_options_str_list opt =
  [
   (out_options_str,
    (out_options_type_to_str (val_of_override opt.out_options)));
   (tptp_safe_out_str, (string_of_bool opt.tptp_safe_out));
   (problem_path_str, opt.problem_path);
   (include_path_str, opt.include_path);
   (clausifier_str, opt.clausifier);
   (clausifier_options_str, opt.clausifier_options);
   (stdin_str, (string_of_bool opt.stdin));
   (dbg_backtrace_str, (string_of_bool opt.dbg_backtrace));
   (dbg_dump_prop_clauses_str, (string_of_bool opt.dbg_dump_prop_clauses));
   (dbg_dump_prop_clauses_file_str,
    opt.dbg_dump_prop_clauses_file);
   (dbg_out_stat_str, (string_of_bool opt.dbg_out_stat))
 ]

let general_options_str_list opt =
  [
   (fof_str, (string_of_bool opt.fof));
   (time_out_real_str, (string_of_float opt.time_out_real));
   (time_out_virtual_str, (string_of_float opt.time_out_virtual));
   (schedule_str, (schedule_type_to_str opt.schedule));
   (ground_splitting_str, (ground_splitting_type_to_str opt.ground_splitting));
   (non_eq_to_eq_str, (string_of_bool opt.non_eq_to_eq));
   (prep_gs_sim_str, (string_of_bool opt.prep_gs_sim));
   (prep_res_sim_str, (string_of_bool opt.prep_res_sim)); 
   (res_sim_input_str, (string_of_bool opt.res_sim_input));
   (clause_weak_htbl_str, (string_of_bool opt.clause_weak_htbl));
   (gc_record_bc_elim_str, (string_of_bool opt.gc_record_bc_elim));
   (symbol_type_check_str, (string_of_bool opt.symbol_type_check));
   (clausify_out_str, (string_of_bool opt.clausify_out));
   (large_theory_mode_str, (string_of_bool opt.large_theory_mode));
   (prep_sem_filter_str, (prep_sem_filter_type_to_str opt.prep_sem_filter));
   (prep_sem_filter_out_str, (string_of_bool opt.prep_sem_filter_out));
   (sub_typing_str, (string_of_bool opt.sub_typing));
   (brand_transform_str, (string_of_bool opt.brand_transform));
   (min_unsat_core_str, (string_of_bool opt.min_unsat_core));
   (prolific_symb_bound_str, (string_of_int opt.prolific_symb_bound));
   (lt_threshold_str, (string_of_int opt.lt_threshold));
 ]

let sat_options_str_list opt =
  [
   (sat_mode_str, (string_of_bool opt.sat_mode));
   (sat_gr_def_str, (string_of_bool opt.sat_gr_def));
   (sat_epr_types_str, (string_of_bool opt.sat_epr_types));
   (sat_non_cyclic_types_str, (string_of_bool opt.sat_non_cyclic_types));
   (sat_finite_models_str, (string_of_bool opt.sat_finite_models));
   (sat_out_model_str, (sat_out_model_type_to_str opt.sat_out_model));
   (sat_out_clauses_str, (string_of_bool opt.sat_out_clauses))
 ]

let bmc1_options_str_list opt =
  [
   (bmc1_incremental_str,
    (string_of_bool (val_of_override opt.bmc1_incremental)));
   (bmc1_axioms_str,
    (bmc1_axioms_type_to_str (val_of_override opt.bmc1_axioms)));
   (bmc1_min_bound_str, (string_of_int (val_of_override opt.bmc1_min_bound)));
   (bmc1_max_bound_str, (string_of_int (val_of_override opt.bmc1_max_bound)));
   (bmc1_max_bound_default_str,
    (string_of_int (val_of_override opt.bmc1_max_bound_default)));
   (bmc1_symbol_reachability_str,
    (string_of_bool opt.bmc1_symbol_reachability));
   (bmc1_add_unsat_core_str,
    (bmc1_add_unsat_core_type_to_str
       (val_of_override opt.bmc1_add_unsat_core)));
   (bmc1_unsat_core_children_str,
    (string_of_bool (val_of_override opt.bmc1_unsat_core_children)));
   (bmc1_unsat_core_extrapolate_axioms_str,
    (string_of_bool (val_of_override opt.bmc1_unsat_core_extrapolate_axioms)));
   (bmc1_out_stat_str,
    (bmc1_out_stat_type_to_str (val_of_override opt.bmc1_out_stat)));
   (bmc1_pre_inst_next_state_str, (string_of_bool opt.bmc1_pre_inst_next_state));
   (bmc1_pre_inst_state_str, (string_of_bool opt.bmc1_pre_inst_state));
   (bmc1_pre_inst_reach_state_str, (string_of_bool opt.bmc1_pre_inst_reach_state));
   (bmc1_out_unsat_core_str,
    (string_of_bool (val_of_override opt.bmc1_out_unsat_core)));
   (bmc1_verbose_str, (string_of_bool (val_of_override opt.bmc1_verbose)));
   (bmc1_dump_clauses_tptp_str,
    (string_of_bool (val_of_override opt.bmc1_dump_clauses_tptp)));
   (bmc1_dump_unsat_core_tptp_str,
    (string_of_bool (val_of_override opt.bmc1_dump_unsat_core_tptp)));
   (bmc1_dump_file_str,
    (string_of_string_option "-" (val_of_override opt.bmc1_dump_file)));
 ]

let inst_options_str_list opt =
  [
   (instantiation_flag_str, (string_of_bool opt.instantiation_flag));
   (inst_lit_sel_str, (inst_lit_sel_type_to_str opt.inst_lit_sel));
   (inst_solver_per_active_str, (string_of_int opt.inst_solver_per_active));
   (inst_solver_per_clauses_str, (string_of_int opt.inst_solver_per_clauses));
   (inst_pass_queue1_str,
    (pass_queue_type_to_str (val_of_override opt.inst_pass_queue1)));
   (inst_pass_queue2_str,
    (pass_queue_type_to_str (val_of_override opt.inst_pass_queue2)));
   (inst_pass_queue3_str,
    (pass_queue_type_to_str (val_of_override opt.inst_pass_queue3)));
   (inst_pass_queue1_mult_str,
    (string_of_int (val_of_override opt.inst_pass_queue1_mult)));
   (inst_pass_queue2_mult_str,
    (string_of_int (val_of_override opt.inst_pass_queue2_mult)));
   (inst_pass_queue3_mult_str,
    (string_of_int (val_of_override opt.inst_pass_queue3_mult)));
   (inst_dismatching_str, (string_of_bool opt.inst_dismatching));
   (inst_eager_unprocessed_to_passive_str, (string_of_bool opt.inst_eager_unprocessed_to_passive));
   (inst_prop_sim_given_str, (string_of_bool opt.inst_prop_sim_given));
   (inst_prop_sim_new_str, (string_of_bool opt.inst_prop_sim_new));
   (inst_orphan_elimination_str, (string_of_bool opt.inst_orphan_elimination));
   (inst_learning_loop_flag_str, (string_of_bool opt.inst_learning_loop_flag));
   (inst_learning_start_str, (string_of_int opt.inst_learning_start));
   (inst_learning_factor_str, (string_of_int opt.inst_learning_factor));
   (inst_start_prop_sim_after_learn_str, (string_of_int opt.inst_start_prop_sim_after_learn));
   (inst_sel_renew_str, (inst_sel_renew_type_to_str opt.inst_sel_renew));
   (inst_lit_activity_flag_str, (string_of_bool opt.inst_lit_activity_flag));
   (inst_out_proof_str,
    (string_of_bool (val_of_override opt.inst_out_proof)));
 ]

let res_options_str_list opt =
  [
   (resolution_flag_str, (string_of_bool opt.resolution_flag));
   (res_lit_sel_str, (res_lit_sel_type_to_str opt.res_lit_sel));
   (res_to_prop_solver_str, (res_to_prop_solver_type_to_str opt.res_to_prop_solver));
   (res_prop_simpl_new_str, (string_of_bool opt.res_prop_simpl_new));
   (res_prop_simpl_given_str, (string_of_bool opt.res_prop_simpl_given));
   (res_passive_queue_flag_str, (string_of_bool opt.res_passive_queue_flag));
   (res_pass_queue1_str, (pass_queue_type_to_str opt.res_pass_queue1));
   (res_pass_queue2_str, (pass_queue_type_to_str opt.res_pass_queue2));
   (res_pass_queue1_mult_str, (string_of_int opt.res_pass_queue1_mult));
   (res_pass_queue2_mult_str, (string_of_int opt.res_pass_queue2_mult));
   (res_forward_subs_str, (res_subs_type_to_str opt.res_forward_subs));
   (res_backward_subs_str, (res_subs_type_to_str opt.res_backward_subs));
   (res_forward_subs_resolution_str, (string_of_bool opt.res_forward_subs_resolution));
   (res_backward_subs_resolution_str, (string_of_bool opt.res_backward_subs_resolution));
   (res_orphan_elimination_str, (string_of_bool opt.res_orphan_elimination));
   (res_time_limit_str, (string_of_float opt.res_time_limit));
   (res_out_proof_str, (string_of_bool opt.res_out_proof))
 ]

let comb_options_str_list opt =
  [
   (comb_res_mult_str, (string_of_int opt.comb_res_mult));
   (comb_inst_mult_str, (string_of_int opt.comb_inst_mult));
 ]

(*

  (_str, opt.);
  (_str, (_type_to_str opt.));
  (_str, (string_of_ opt.));

 *)

let input_opt_str opt =
  "\n"^(s_pref_str ())^"Input Options\n\n"^
  opt_val_list_to_str (input_options_str_list opt)^"\n"

let general_opt_str opt =
  "\n"^(s_pref_str ())^"General Options\n\n"^
  opt_val_list_to_str (general_options_str_list opt)^"\n"

let sat_options_str opt =
  "\n"^(s_pref_str ())^"SAT Options\n\n"^
  opt_val_list_to_str (sat_options_str_list opt)^"\n"

let bmc1_opt_str opt =
  "\n"^(s_pref_str ())^"BMC1 Options\n\n"^
  opt_val_list_to_str (bmc1_options_str_list opt)^"\n"

let inst_opt_str opt =
  "\n"^(s_pref_str ())^"Instantiation Options\n\n"^
  opt_val_list_to_str (inst_options_str_list opt)^"\n"

let res_opt_str opt =
  "\n"^(s_pref_str ())^"Resolution Options\n\n"^
  opt_val_list_to_str (res_options_str_list opt)^"\n"

let comb_opt_str opt =
  "\n"^(s_pref_str ())^"Combination Options\n\n"^
  opt_val_list_to_str (comb_options_str_list opt)^"\n"

let control_opt_str opt =
  (general_opt_str opt)^
  (sat_options_str opt)^
  (bmc1_opt_str opt)^
  (inst_opt_str opt)^
  (res_opt_str opt)^
  (comb_opt_str opt)

let all_opt_str opt =
  (input_opt_str opt)^(control_opt_str opt)

let options_to_str opt =
  let close_str = (s_pref_str ())^"\n" in
  (*(pref_str^(out_options_type_to_str opt.out_options)^"\n";*)
  match val_of_override opt.out_options with
  | Out_All_Opt -> (all_opt_str opt)^close_str
  | Out_Control_Opt -> (control_opt_str opt)^close_str
  | Out_No_Opt -> ""

(* inferred options: *)

let prop_solver_is_on () =
  !current_options.instantiation_flag ||
  !current_options.res_prop_simpl_new ||
  !current_options.res_prop_simpl_given ||
  !current_options.prep_gs_sim ||
  !current_options.prep_res_sim ||
  (match !current_options.res_to_prop_solver with
    Res_to_Solver_Active | Res_to_Solver_Passive -> true
  | Res_to_Solver_None -> false)

(*-------------Read Current Options--------------------------*)

let usage_msg = "iproveropt [options] [filename]\n\n"
    (* ugly hack, redo via format later *)
  ^(dash_str "Input Options")^"\n"

let help_msg = "--help  Display list of options\n"

(*
  let read_args() =
  Arg.parse spec_list default_arg_fun usage_msg
 *)

let read_args() =
  let args = Sys.argv in
  (* let iprover_name = args.(0) in
     let current = Arg.current in *)
  try
    Arg.parse_argv args spec_list default_arg_fun usage_msg
  with
    
  | Arg.Bad s -> (
      let str_list = Str.split (Str.regexp "\n") s in
      out_str ((List.hd str_list)^"\n\n"
	       ^"Usage: "^usage_msg^"\n"^help_msg);
      (*
	out_str (s^ipr_name^": "^"unknown option "
	^"`"^(args.(!current))^"'"^"\n \n"
	^usage_msg^"\n"^help_msg);
       *)
      exit (1))
	
  | Arg.Help s -> (out_str (s); exit (0))

let check_options_consistency () =
  (if (!current_options.problem_files = [] && (not !current_options.stdin))
  then
    ((*Arg.usage spec_list usage_msg;*)
     out_str (usage_msg^"\n"^help_msg);
     failwith "No problem files to solve")
  else ()
  );
  (
   if (!current_options.bmc1_pre_inst_state) && ((not !current_options.bmc1_pre_inst_next_state) || (not !current_options.bmc1_pre_inst_reach_state))
   then
     failwith "if \"--bmc1_pre_inst_state true\" then it  should be --bmc1_pre_inst_next_state true and --bmc1_pre_inst_reach_state true"
   else ()
  );
  (
   if (!current_options.sat_finite_models && (not !current_options.sat_mode))
   then
     failwith "if --sat_finite_model true then --sat_mode should be also true"
  )

let () = read_args();
  check_options_consistency ()

let get_problem_files () = !current_options.problem_files

(*-------------------------------------------------------------------*)
(*----- Some predefined options we will use in schedules-------------*)

type named_options = { options_name : string; options : options }

(*creates a fresh copy of the option*)
(* we need to use dummy out_options = option.out_options *)
let copy_options option = { option with out_options = option.out_options }

(* Input Options *)
let input_options = copy_options !current_options

let input_named_options =
  { options_name = "Input Options"; options = input_options }

(*--------------------------------*)

let strip_conj_named_opt named_opt =
  let new_opt =
    { named_opt.options with
      
      inst_lit_sel =
      strip_conj_lit_type_list named_opt.options.inst_lit_sel;
      
      inst_pass_queue1 =
      override_value
	named_opt.options.inst_pass_queue1
	(strip_conj_clause_type_list
	   (val_of_override named_opt.options.inst_pass_queue1));
      
      inst_pass_queue2 =
      override_value
	named_opt.options.inst_pass_queue2
	(strip_conj_clause_type_list
	   (val_of_override named_opt.options.inst_pass_queue2));
      
      inst_pass_queue3 =
      override_value
	named_opt.options.inst_pass_queue3
	(strip_conj_clause_type_list
	   (val_of_override named_opt.options.inst_pass_queue3));
      
      res_pass_queue1 =
      strip_conj_clause_type_list named_opt.options.res_pass_queue1;
      
      res_pass_queue2 =
      strip_conj_clause_type_list named_opt.options.res_pass_queue2;
      
    }
  in
  { options = new_opt;
    options_name = (named_opt.options_name^" stripped conjectures") }

(*--------Creates a reasonable option to deal with many axioms such as SUMO-----*)
(*-------based on a given option-------------------*)
let named_opt_to_many_axioms_named_opt1 opt =
  let new_options =
    { opt.options with
      
      large_theory_mode = true;
      prep_sem_filter = Sem_Filter_Neg;
      prep_sem_filter_out = false;
      prolific_symb_bound = 500;
      lt_threshold = 2000;
      
      inst_pass_queue1 =
      ValueDefault
	[Cl_Conj_Dist false;
	 Cl_Has_Non_Prolific_Conj_Symb true;
	 Cl_Num_of_Var false];
      
      inst_pass_queue1_mult = ValueDefault 1000;
      inst_pass_queue2_mult = ValueDefault 2;
      
      inst_pass_queue3 = ValueDefault [];
      inst_pass_queue3_mult = ValueDefault 0;
      
      res_pass_queue1 = [Cl_Conj_Dist false;
			 Cl_Has_Non_Prolific_Conj_Symb true;
			 Cl_Num_of_Symb false];
      
      res_pass_queue1_mult = 1000;
      res_pass_queue2_mult = 5;
      res_backward_subs = Subs_Subset;
      res_forward_subs_resolution = true;
      res_backward_subs_resolution = false;
      res_orphan_elimination = false;
    }
  in
  { options_name = ("Many Axioms 1 "^opt.options_name);
    options = new_options }

(*----------Many Axioms 2-----------------------*)
let named_opt_to_many_axioms_named_opt2 opt =
  let new_options =
    { opt.options with
      
      large_theory_mode = true;
      prep_sem_filter = Sem_Filter_Neg;
      prep_sem_filter_out = false;
      prolific_symb_bound = 500;
      lt_threshold = 2000;
      
      inst_pass_queue1 =
      ValueDefault
	[Cl_Conj_Dist false;
	 Cl_Has_Non_Prolific_Conj_Symb true;
	 (*Cl_Max_Atom_Input_Occur false;*)
	 Cl_Num_of_Var false];
      
      (*	inst_solver_per_active = 200;
	inst_solver_per_clauses = 1000;
       *)
      
      inst_pass_queue1_mult = ValueDefault 1000;
      inst_pass_queue2_mult = ValueDefault 2;
      
      inst_pass_queue3 = ValueDefault [];
      inst_pass_queue3_mult = ValueDefault 0;
      
      inst_prop_sim_given = false;
      inst_prop_sim_new = false;
      inst_orphan_elimination = !current_options.inst_orphan_elimination;
      inst_learning_start = 3000000;
      inst_learning_factor = 2;
      
      res_pass_queue1 = [Cl_Conj_Dist false;
			 Cl_Has_Non_Prolific_Conj_Symb true;
			 Cl_Num_of_Var false;
			 (*Cl_Max_Atom_Input_Occur false*)];
      
      res_prop_simpl_new = false;
      res_prop_simpl_given = false;
      
      res_pass_queue1_mult = 1000;
      res_pass_queue2_mult = 2;
      
      res_forward_subs = Subs_Subset;
      res_backward_subs = Subs_Subset;
      res_forward_subs_resolution = false;
      res_backward_subs_resolution = false;
      res_orphan_elimination = false;
      comb_res_mult = 100;
      comb_inst_mult = 1000;
    }
  in
  { options_name = ("Many Axioms 2 "^opt.options_name);
    options = new_options }

(*------------------------------------------------*)

let named_opt_to_many_axioms_named_opt3 opt =
  let new_options =
    { opt.options with
      
      large_theory_mode = true;
      prep_sem_filter = Sem_Filter_Neg;
      prep_sem_filter_out = false;
      prolific_symb_bound = 500;
      lt_threshold = 2000;
      
      inst_pass_queue1 =
      ValueDefault
	[Cl_Conj_Dist false;
	 Cl_Has_Non_Prolific_Conj_Symb true;
	 Cl_Num_of_Var false;
	 Cl_Max_Atom_Input_Occur false];
      
      inst_pass_queue1_mult = ValueDefault 1000;
      inst_pass_queue2_mult = ValueDefault 2;
      
      inst_pass_queue3 = ValueDefault [];
      inst_pass_queue3_mult = ValueDefault 0;
      
      res_pass_queue1 = [Cl_Conj_Dist false;
			 Cl_Has_Non_Prolific_Conj_Symb true;
			 Cl_Num_of_Symb false; Cl_Max_Atom_Input_Occur false];
      
      res_pass_queue1_mult = 1000;
      res_pass_queue2_mult = 5;
      res_backward_subs = Subs_Subset;
      res_forward_subs_resolution = true;
      res_backward_subs_resolution = false;
      res_orphan_elimination = false;
    }
  in
  { options_name = ("Many Axioms 3 "^opt.options_name);
    options = new_options }

(*-------Negative Selections------------------------*)
let option_1 () = {

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;
  
  (*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  clausifier = !current_options.clausifier;
  clausifier_options = !current_options.clausifier_options;
  stdin = !current_options.stdin;
  dbg_backtrace = !current_options.dbg_backtrace;
  dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
  dbg_dump_prop_clauses_file =
  !current_options.dbg_dump_prop_clauses_file;
  dbg_out_stat = !current_options.dbg_out_stat;

  (*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;
  ground_splitting = !current_options.ground_splitting;
  non_eq_to_eq = false;
  prep_gs_sim = !current_options.prep_gs_sim;
  prep_res_sim = !current_options.prep_res_sim;
  res_sim_input = !current_options.res_sim_input;
  clause_weak_htbl = !current_options.clause_weak_htbl; (* should not be chnaged from input options *)
  gc_record_bc_elim = !current_options.gc_record_bc_elim;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;
  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  sub_typing = !current_options.sub_typing;
  brand_transform = !current_options.brand_transform;
  min_unsat_core = !current_options.min_unsat_core;
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*----Sat Mode------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_epr_types = !current_options.sat_epr_types;
  sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;
  sat_out_clauses = !current_options.sat_out_clauses;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----Instantiation------*)
  instantiation_flag = true;
  inst_lit_sel = [Lit_Sign false;
		  Lit_Num_of_Var false; Lit_Num_of_Symb true];
  
  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  
  inst_pass_queue1 =
  ValueDefault
    [Cl_Conj_Dist false;
     Cl_Has_Conj_Symb true;
     Cl_Num_of_Var false];
  
  inst_pass_queue2 =
  ValueDefault
    [Cl_Age true;
     Cl_Num_of_Symb false];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 25;
  inst_pass_queue2_mult = ValueDefault 2;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  inst_dismatching = true;
  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = true;
  inst_orphan_elimination = !current_options.inst_orphan_elimination;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Model;
  inst_lit_activity_flag = true;
  inst_out_proof = ValueDefault true;
  
  (*----Resolution---------*)
  resolution_flag = true;
  res_lit_sel = Res_Neg_Sel_Max;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Conj_Dist false; Cl_Has_Conj_Symb true;
		     Cl_Num_of_Symb false];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 5;
  
  res_forward_subs = Subs_Full;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = true;
  (*  res_forward_subs_resolution    = true; exp later for sat *)
  (* res_backward_subs_resolution   = false; *)
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 2.0;
  res_out_proof = !current_options.res_out_proof;
  (*----Combination--------*)
  comb_res_mult = 300;
  comb_inst_mult = 1000;
}

let named_option_1 () =
  { options_name = "Option_1: Negative Selections"; options = (option_1()) }

(*--------------*)
let option_1_1 () = { (input_options) with
		      
		      inst_lit_sel = [Lit_Sign false;
				      Lit_Num_of_Var false;
				      Lit_Num_of_Symb true];
		      res_lit_sel = Res_Neg_Sel_Max
		    }

let named_option_1_1 () =
  { options_name = "Option_1_1: Negative Selections"; options = (option_1_1()) }

(*--------------*)

let option_1_2 () = { (input_options) with
		      
		      inst_pass_queue1 =
		      ValueDefault
			[Cl_Conj_Dist false;
			 Cl_Has_Conj_Symb true;
			 Cl_EPR true;
			 Cl_Num_of_Var false];
		      
		      inst_pass_queue2 =
		      ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
		      
		      inst_pass_queue3 = ValueDefault [];
		      inst_pass_queue3_mult = ValueDefault 0;
		      
		      res_pass_queue1 = [Cl_Conj_Dist false; Cl_Has_Conj_Symb true;
					 Cl_Horn true;
					 Cl_Num_of_Symb false];
		      res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];

		    }

let named_option_1_2 () =
  { options_name = "Option_1_2: EPR, Horn"; options = (option_1_2()) }

(*--Option 2----------------*)

let option_2 () = {

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;
  
  (*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  clausifier = !current_options.clausifier;
  clausifier_options = !current_options.clausifier_options;
  stdin = !current_options.stdin;
  dbg_backtrace = !current_options.dbg_backtrace;
  dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
  dbg_dump_prop_clauses_file =
  !current_options.dbg_dump_prop_clauses_file;
  dbg_out_stat = !current_options.dbg_out_stat;
  
  (*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;
  ground_splitting = !current_options.ground_splitting;
  non_eq_to_eq = false;
  prep_gs_sim = !current_options.prep_gs_sim;
  prep_res_sim = !current_options.prep_res_sim;
  res_sim_input = !current_options.res_sim_input;
  clause_weak_htbl = !current_options.clause_weak_htbl;
  gc_record_bc_elim = !current_options.gc_record_bc_elim;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;
  
  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  sub_typing = !current_options.sub_typing;
  brand_transform = !current_options.brand_transform;
  min_unsat_core = !current_options.min_unsat_core;
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*----Sat Mode--------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_epr_types = !current_options.sat_epr_types;
  sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;
  sat_out_clauses = !current_options.sat_out_clauses;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----Instantiation------*)
  instantiation_flag = true;
  inst_lit_sel = [Lit_Sign false;
		  Lit_Num_of_Var false; Lit_Num_of_Symb false];
  
  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  
  inst_pass_queue1 =
  ValueDefault
    [Cl_Num_of_Symb false;
     Cl_Num_of_Var false;
     Cl_Conj_Dist false;
     Cl_Has_Conj_Symb true];
  
  inst_pass_queue2 = ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 25;
  inst_pass_queue2_mult = ValueDefault 2;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  inst_dismatching = true;
  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = true;
  inst_orphan_elimination = !current_options.inst_orphan_elimination;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Model;
  inst_lit_activity_flag = true;
  inst_out_proof = ValueDefault true;
  
  (*----Resolution---------*)
  resolution_flag = true;
  res_lit_sel = Res_KBO_Max;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Num_of_Symb false; Cl_Has_Conj_Symb true; ];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 5;
  
  res_forward_subs = Subs_Full;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = true;
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 2.0;
  res_out_proof = !current_options.res_out_proof;
  (*----Combination--------*)
  comb_res_mult = 300;
  comb_inst_mult = 1000;
}

let named_option_2 () =
  { options_name = "Option_2: Max Selections"; options = (option_2()) }

let option_2_1 () = { (option_2 ()) with
		      inst_lit_sel = [Lit_Sign false;
				      Lit_Num_of_Var false;
				      Lit_Num_of_Symb true];
		      
		      res_lit_sel = Res_KBO_Max;
		    }

let named_option_2_1 () =
  { options_name = "Option_2_1: Max Selections"; options = (option_2_1()) }

(*--Option 3----------------*)

let option_3 () = {

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;
  
  (*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  clausifier = !current_options.clausifier;
  clausifier_options = !current_options.clausifier_options;
  stdin = !current_options.stdin;
  dbg_backtrace = !current_options.dbg_backtrace;
  dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
  dbg_dump_prop_clauses_file =
  !current_options.dbg_dump_prop_clauses_file;
  dbg_out_stat = !current_options.dbg_out_stat;
  
  (*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;
  ground_splitting = !current_options.ground_splitting;
  non_eq_to_eq = false;
  prep_gs_sim = !current_options.prep_gs_sim;
  prep_res_sim = !current_options.prep_res_sim;
  res_sim_input = !current_options.res_sim_input;
  clause_weak_htbl = !current_options.clause_weak_htbl;
  gc_record_bc_elim = !current_options.gc_record_bc_elim;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;
  
  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  sub_typing = !current_options.sub_typing;
  brand_transform = !current_options.brand_transform;
  min_unsat_core = !current_options.min_unsat_core;
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*----Sat Mode--------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_epr_types = !current_options.sat_epr_types;
  sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;
  sat_out_clauses = !current_options.sat_out_clauses;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----Instantiation------*)
  instantiation_flag = true;
  inst_lit_sel = [Lit_Sign false; Lit_Num_of_Symb false];
  
  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  
  inst_pass_queue1 =
  ValueDefault
    [Cl_Num_of_Symb false;
     Cl_Conj_Dist false;
     Cl_Has_Conj_Symb true];
  
  inst_pass_queue2 = ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 25;
  inst_pass_queue2_mult = ValueDefault 2;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  inst_dismatching = true;
  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = true;
  inst_orphan_elimination = !current_options.inst_orphan_elimination;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Model;
  inst_lit_activity_flag = true;
  inst_out_proof = ValueDefault true;
  
  (*----Resolution---------*)
  resolution_flag = true;
  res_lit_sel = Res_Neg_Sel_Min;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Num_of_Symb false; Cl_Has_Conj_Symb true; ];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 5;
  
  res_forward_subs = Subs_Full;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = true;
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 2.0;
  res_out_proof = !current_options.res_out_proof;
  (*----Combination--------*)
  comb_res_mult = 300;
  comb_inst_mult = 1000;
}

let named_option_3 () =
  { options_name = "Option_3: Min Selections"; options = (option_3()) }

let option_3_1 () = { (input_options) with
		      inst_lit_sel = [Lit_Sign false; Lit_Num_of_Symb true];
		      res_lit_sel = Res_Neg_Sel_Min;
		    }

let named_option_3_1 () =
  { options_name = "Option_3_1: Min Selections"; options = (option_3_1()) }

(*--Option 4----------------*)

let option_4 () = {

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;
  
  (*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  clausifier = !current_options.clausifier;
  clausifier_options = !current_options.clausifier_options;
  stdin = !current_options.stdin;
  dbg_backtrace = !current_options.dbg_backtrace;
  dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
  dbg_dump_prop_clauses_file =
  !current_options.dbg_dump_prop_clauses_file;
  dbg_out_stat = !current_options.dbg_out_stat;
  
  (*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;
  ground_splitting = !current_options.ground_splitting;
  non_eq_to_eq = false;
  prep_gs_sim = !current_options.prep_gs_sim;
  prep_res_sim = !current_options.prep_res_sim;
  res_sim_input = !current_options.res_sim_input;
  clause_weak_htbl = !current_options.clause_weak_htbl;
  gc_record_bc_elim = !current_options.gc_record_bc_elim;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;
  
  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  sub_typing = !current_options.sub_typing;
  brand_transform = !current_options.brand_transform;
  min_unsat_core = !current_options.min_unsat_core;
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*----Sat Mode--------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_epr_types = !current_options.sat_epr_types;
  sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;
  sat_out_clauses = !current_options.sat_out_clauses;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----Instantiation------*)
  instantiation_flag = true;
  inst_lit_sel = [Lit_Sign true; Lit_Num_of_Var false; Lit_Num_of_Symb false];
  
  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  
  inst_pass_queue1 =
  ValueDefault [Cl_Has_Conj_Symb true; Cl_Num_of_Symb false ];
  
  inst_pass_queue2 = ValueDefault [Cl_Age true;];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 25;
  inst_pass_queue2_mult = ValueDefault 10;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  inst_dismatching = true;
  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = true;
  inst_orphan_elimination = !current_options.inst_orphan_elimination;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Model;
  inst_lit_activity_flag = true;
  inst_out_proof = ValueDefault true;
  
  (*----Resolution---------*)
  resolution_flag = true;
  res_lit_sel = Res_Adaptive;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Has_Conj_Symb true; ];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 10;
  
  res_forward_subs = Subs_Full;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = false;
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 2.0;
  res_out_proof = !current_options.res_out_proof;
  (*----Combination--------*)
  comb_res_mult = 300;
  comb_inst_mult = 1000;
}

let named_option_4 () =
  { options_name = "Option_4: Selections"; options = (option_4()) }

let option_4_1 () = { (input_options) with
		      inst_lit_sel = [Lit_Sign true; Lit_Num_of_Var false; Lit_Num_of_Symb false];
		      res_lit_sel = Res_Adaptive;
		    }

let named_option_4_1 () =
  { options_name = "Option_4_1: Selections"; options = (option_4_1()) }

(*------Finite Models--------------------------------------*)
let named_opt_sat_mode_off named_opt =
  { options_name = named_opt.options_name^" sat_mode off";
    options = { named_opt.options with
		sat_mode = false; sat_finite_models = false; sat_out_model = Model_Small }}

let named_opt_sat_mode_on named_opt =
  { options_name = named_opt.options_name^" sat_mode on";
    options = { named_opt.options with sat_mode = true; sat_finite_models = true; }}

let option_finite_models () = {

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;
  
  (*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  clausifier = !current_options.clausifier;
  clausifier_options = !current_options.clausifier_options;
  stdin = !current_options.stdin;
  dbg_backtrace = !current_options.dbg_backtrace;
  dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
  dbg_dump_prop_clauses_file =
  !current_options.dbg_dump_prop_clauses_file;
  dbg_out_stat = !current_options.dbg_out_stat;
  
  (*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = Schedule_none;
  ground_splitting = !current_options.ground_splitting; (* input_options.ground_splitting;*)
  non_eq_to_eq = false;
  prep_gs_sim = !current_options.prep_gs_sim;
  prep_res_sim = !current_options.prep_res_sim;
  res_sim_input = !current_options.res_sim_input;
  clause_weak_htbl = !current_options.clause_weak_htbl;
  gc_record_bc_elim = !current_options.gc_record_bc_elim;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;
  
  large_theory_mode = false;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  sub_typing = !current_options.sub_typing;
  brand_transform = false;
  min_unsat_core = !current_options.min_unsat_core;
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*----Sat Mode-----*)
  sat_mode = true;
  sat_gr_def = false;
  sat_epr_types = !current_options.sat_epr_types;
  sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
  sat_finite_models = true;
  sat_out_model = !current_options.sat_out_model;
  sat_out_clauses = !current_options.sat_out_clauses;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----Instantiation------*)
  instantiation_flag = true;
  
  inst_lit_sel = [Lit_Sign false; Lit_Ground true;
		  Lit_Num_of_Var false; Lit_Num_of_Symb false];
  (*
    inst_lit_sel = [Lit_Sign true;
    Lit_Num_of_Var false; Lit_Num_of_Symb false];
   *)
  (*
    inst_lit_sel = [ Lit_Ground true; Lit_Sign false;
    Lit_Num_of_Var true; Lit_Num_of_Symb false];
   *)
  
  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  
  inst_pass_queue1 =
  ValueDefault [Cl_Num_of_Var false; Cl_Num_of_Symb false];
  
  inst_pass_queue2 =
  ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 20;
  inst_pass_queue2_mult = ValueDefault 10;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  inst_dismatching = true;
  inst_eager_unprocessed_to_passive = true;
  
  (* should not prop simplify! can lead to inconsistency  *)
  inst_prop_sim_given = false;
  inst_prop_sim_new = false;
  inst_orphan_elimination = !current_options.inst_orphan_elimination;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Model;
  inst_lit_activity_flag = true;
  inst_out_proof = ValueDefault true;
  
  (*----Resolution---------*)
  (*---always resolution_flag false-------------------*)
  resolution_flag = false;
  res_lit_sel = Res_Adaptive;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Conj_Dist false; Cl_Has_Conj_Symb true;
		     Cl_Num_of_Symb false];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 5;
  
  res_forward_subs = Subs_Full;
  res_backward_subs = Subs_Full;
  res_forward_subs_resolution = true;
  res_backward_subs_resolution = true;
  res_orphan_elimination = true;
  res_time_limit = 2.0;
  res_out_proof = !current_options.res_out_proof;
  (*----Combination--------*)
  comb_res_mult = 1;
  comb_inst_mult = 1000;
}

let named_option_finite_models () =
  { options_name = "Option: Finite Models"; options = (option_finite_models()) }

(*------------------------------------*)
let option_epr_non_horn () = {
(*------------------------------------*)

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;
  
  (*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  clausifier = !current_options.clausifier;
  clausifier_options = !current_options.clausifier_options;
  stdin = !current_options.stdin;
  dbg_backtrace = !current_options.dbg_backtrace;
  dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
  dbg_dump_prop_clauses_file =
  !current_options.dbg_dump_prop_clauses_file;
  dbg_out_stat = !current_options.dbg_out_stat;
  
  (*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;
  ground_splitting = !current_options.ground_splitting;
  non_eq_to_eq = false;
  prep_gs_sim = !current_options.prep_gs_sim;
  prep_res_sim = !current_options.prep_res_sim;
  res_sim_input = !current_options.res_sim_input;
  clause_weak_htbl = !current_options.clause_weak_htbl;
  gc_record_bc_elim = !current_options.gc_record_bc_elim;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;
  
  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  sub_typing = !current_options.sub_typing;
  brand_transform = false;
  min_unsat_core = !current_options.min_unsat_core;
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*----Sat Mode--------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_epr_types = !current_options.sat_epr_types;
  sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;
  sat_out_clauses = !current_options.sat_out_clauses;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----Instantiation------*)
  instantiation_flag = true;
  (*------------------------------------------*)
  inst_lit_sel = [Lit_Ground true; Lit_Sign false;];
  
  (* before Intel example bpbimodalm_miter_full.focnf.bit_blast.Mclk1 *)
  (* inst_solver_per_active         = 750; after 7500 *)
  (*  inst_solver_per_active         = 750;*)
  (*  inst_solver_per_active         = 7500;*)
  
  inst_solver_per_active = !current_options.inst_solver_per_active;
  
  (* inst_solver_per_clauses        = 5000; is ok*)
  (*  inst_solver_per_clauses        = 5000;*)
  inst_solver_per_clauses = !current_options.inst_solver_per_clauses;
  
  inst_pass_queue1 =
  ValueDefault
    [Cl_Conj_Dist false;
     Cl_Has_Conj_Symb true;
     (*			    Cl_Ground true;*)
     Cl_Num_of_Var false];
  
  inst_pass_queue2 = ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 25;
  inst_pass_queue2_mult = ValueDefault 20;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  (* befor ok inst_dismatching               = false;*)
  inst_dismatching = false;
  (*  inst_dismatching               = false;*)
  (*  inst_dismatching               =  !current_options.inst_dismatching;*)
  
  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = false;
  inst_orphan_elimination = !current_options.inst_orphan_elimination;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Solver;
  inst_lit_activity_flag = false;
  (*  inst_lit_activity_flag            = true;*)
  inst_out_proof = ValueDefault true;
  
  (*----Resolution----------------------------*)
  resolution_flag = true;
  (*------------------------------------------*)
  res_lit_sel = Res_Adaptive;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Has_Conj_Symb true; ];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 10;
  
  res_forward_subs = Subs_Subset;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = false;
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 0.1;
  res_out_proof = !current_options.res_out_proof;
  (*----Combination--------*)
  comb_res_mult = 30;
  comb_inst_mult = 100;
}

(*
(* options epr_non_horn CASC09 *)
(*------------------------------------*)
  let option_epr_non_horn () = {
(*------------------------------------*)

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;

(*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  eprover_path = !current_options.eprover_path;
  stdin = !current_options.stdin;

(*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;
  ground_splitting = Split_Input;
  non_eq_to_eq = false;
  prep_gs_sim = true;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;

  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  prolific_symb_bound = 500;
  lt_threshold = 2000;

(*----Sat Mode--------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;

(*----Instantiation------*)
  instantiation_flag = true;
  inst_lit_sel = [Lit_Ground true; Lit_Sign false;];

(* before Intel example bpbimodalm_miter_full.focnf.bit_blast.Mclk1 *)
(* inst_solver_per_active         = 750; after 7500 *)
(*  inst_solver_per_active         = 750;*)
(*  inst_solver_per_active         = 7500;*)

  inst_solver_per_active = !current_options.inst_solver_per_active;

(* inst_solver_per_clauses        = 5000; is ok*)
(*  inst_solver_per_clauses        = 5000;*)
  inst_solver_per_clauses = !current_options.inst_solver_per_clauses;

  inst_pass_queue1 = [Cl_Conj_Dist false;
  Cl_Has_Conj_Symb true;
(*			    Cl_Ground true;*)
  Cl_Num_of_Var false];
  inst_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];

(*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = 25;
  inst_pass_queue2_mult = 20;

(* befor ok inst_dismatching               = false;*)
  inst_dismatching = false;
(*  inst_dismatching               = false;*)
(*  inst_dismatching               =  !current_options.inst_dismatching;*)

  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = false;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Solver;
  inst_lit_activity_flag = false;

(*----Resolution----------------------------*)
  resolution_flag = false;
(*------------------------------------------*)
  res_lit_sel = Res_Adaptive;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = false;
(*switch between simpl and priority queues*)
(* TO DO  Queues options like in Inst. *)
  res_passive_queue_flag = true;
  res_pass_queue1 = [Cl_Has_Conj_Symb true; ];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 10;

  res_forward_subs = Subs_Subset;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = false;
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 2.0;
  res_out_proof = false;
(*----Combination--------*)
  comb_res_mult = 30;
  comb_inst_mult = 1000;
  }

 *)

let named_option_epr_non_horn () =
  { options_name = "Option_epr_non_horn"; options = (option_epr_non_horn()) }

(*-------------Horn-----------------------*)

(* options from CASC 2008*)

let option_epr_horn () = {

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;
  
  (*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  clausifier = !current_options.clausifier;
  clausifier_options = !current_options.clausifier_options;
  stdin = !current_options.stdin;
  dbg_backtrace = !current_options.dbg_backtrace;
  dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
  dbg_dump_prop_clauses_file =
  !current_options.dbg_dump_prop_clauses_file;
  dbg_out_stat = !current_options.dbg_out_stat;
  
  (*----General--------*)
  
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;
  ground_splitting = !current_options.ground_splitting;
  non_eq_to_eq = false;
  prep_gs_sim = !current_options.prep_gs_sim;
  prep_res_sim = !current_options.prep_res_sim;
  res_sim_input = !current_options.res_sim_input;
  clause_weak_htbl = !current_options.clause_weak_htbl;
  gc_record_bc_elim = !current_options.gc_record_bc_elim;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;
  
  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  sub_typing = !current_options.sub_typing;
  brand_transform = false;
  min_unsat_core = !current_options.min_unsat_core;
  prolific_symb_bound = 500;
  lt_threshold = 2000;
  
  (*----Sat Mode--------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_epr_types = !current_options.sat_epr_types;
  sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;
  sat_out_clauses = !current_options.sat_out_clauses;
  
  (*----BMC1---------------*)
  bmc1_incremental = ValueDefault false;
  bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
  bmc1_min_bound = ValueDefault 0;
  bmc1_max_bound = ValueDefault (-1);
  bmc1_max_bound_default = ValueDefault (-1);
  bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
  bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_None;
  bmc1_unsat_core_children = ValueDefault false;
  bmc1_unsat_core_extrapolate_axioms = ValueDefault false;
  bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
  bmc1_pre_inst_next_state = false;
  bmc1_pre_inst_state = false;
  bmc1_pre_inst_reach_state = false;
  bmc1_out_unsat_core = ValueDefault false;
  bmc1_verbose = ValueDefault false;
  bmc1_dump_clauses_tptp = ValueDefault false;
  bmc1_dump_unsat_core_tptp = ValueDefault false;
  bmc1_dump_file = ValueDefault None;
  
  (*----------------------Instantiation------*)
  instantiation_flag = true;
  (*------------------------------------------*)
  
  inst_lit_sel = [Lit_Sign true; Lit_Ground true; Lit_Num_of_Var false; Lit_Num_of_Symb false];
  
  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  
  inst_pass_queue1 =
  ValueDefault
    [Cl_Conj_Dist false;
     Cl_Has_Conj_Symb true;
     Cl_Num_of_Var false];
  
  inst_pass_queue2 =
  ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
  
  (*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = ValueDefault 25;
  inst_pass_queue2_mult = ValueDefault 5;
  
  inst_pass_queue3 = ValueDefault [];
  inst_pass_queue3_mult = ValueDefault 0;
  
  inst_dismatching = true;
  (*  inst_dismatching               =  !current_options.inst_dismatching;*)
  
  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = true;
  inst_orphan_elimination = !current_options.inst_orphan_elimination;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 3;
  inst_sel_renew = Inst_SR_Solver;
  inst_lit_activity_flag = true;
  inst_out_proof = ValueDefault true;
  
  (*----Resolution----------------------------*)
  resolution_flag = true;
  (*------------------------------------------*)
  res_lit_sel = Res_Neg_Sel_Min;
  (*  res_lit_sel                    = Res_Adaptive;*)
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
  (*switch between simpl and priority queues*)
  (* TO DO  Queues options like in Inst. *)
  (*-----------------------------*)
  res_passive_queue_flag = true;
  (*-----------------------------*)
  res_pass_queue1 = [Cl_Conj_Dist false;
		     Cl_Has_Conj_Symb true;
		     Cl_Num_of_Symb false];
  
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  (*  res_pass_queue1_mult           = 15;*)
  res_pass_queue2_mult = 5;
  
  res_forward_subs = Subs_Subset;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = false;
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 2.;
  res_out_proof = !current_options.res_out_proof;
  (*----Combination--------*)
  comb_res_mult = 1000;
  comb_inst_mult = 300;
(*  comb_inst_mult                 = 300;*)

}
(*

(* Options for CASC 2009 *)

  let option_epr_horn () = {

  out_options = !current_options.out_options;
  tptp_safe_out = !current_options.tptp_safe_out;

(*----Input-------*)
  problem_path = !current_options.problem_path;
  include_path = !current_options.include_path;
  problem_files = !current_options.problem_files;
  eprover_path = !current_options.eprover_path;
  stdin = !current_options.stdin;

(*----General--------*)
  fof = false;
  time_out_real = -1.;
  time_out_virtual = -1.;
  schedule = !current_options.schedule;

  ground_splitting = Split_Input;
  non_eq_to_eq = false;
  prep_gs_sim = true;
  symbol_type_check = !current_options.symbol_type_check;
  clausify_out = false;

  large_theory_mode = true;
  prep_sem_filter = !current_options.prep_sem_filter;
  prep_sem_filter_out = false;
  prolific_symb_bound = 500;
  lt_threshold = 2000;

(*----Sat Mode--------*)
  sat_mode = false;
  sat_gr_def = false;
  sat_finite_models = false;
  sat_out_model = !current_options.sat_out_model;

(*----------------------Instantiation------*)
  instantiation_flag = false;
(*------------------------------------------*)

  inst_lit_sel = [Lit_Sign false; Lit_Ground true;];

  inst_solver_per_active = 750;
  inst_solver_per_clauses = 5000;
  inst_pass_queue1 = [Cl_Conj_Dist false;
  Cl_Has_Conj_Symb true;
  Cl_Ground true;
  Cl_Num_of_Var false];
  inst_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];

(*"[+age;-num_symb]";*)
  inst_pass_queue1_mult = 25;
  inst_pass_queue2_mult = 20;

  inst_dismatching = false;
(*  inst_dismatching               =  !current_options.inst_dismatching;*)

  inst_eager_unprocessed_to_passive = true;
  inst_prop_sim_given = false;
  inst_prop_sim_new = false;
  inst_learning_loop_flag = true;
  inst_learning_start = 3000;
  inst_learning_factor = 2;
  inst_start_prop_sim_after_learn = 300;
  inst_sel_renew = Inst_SR_Solver;
  inst_lit_activity_flag = true;

(*----Resolution----------------------------*)
  resolution_flag = true;
(*------------------------------------------*)
  res_lit_sel = Res_Neg_Sel_Min;
  res_to_prop_solver = Res_to_Solver_Active;
  res_prop_simpl_new = false;
  res_prop_simpl_given = true;
(*switch between simpl and priority queues*)
(* TO DO  Queues options like in Inst. *)
(*-----------------------------*)
  res_passive_queue_flag = false;
(*-----------------------------*)
  res_pass_queue1 = [Cl_Has_Conj_Symb true; ];
  res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
  res_pass_queue1_mult = 15;
  res_pass_queue2_mult = 10;

  res_forward_subs = Subs_Subset;
  res_backward_subs = Subs_Subset;
  res_forward_subs_resolution = false;
  res_backward_subs_resolution = false;
  res_orphan_elimination = false;
  res_time_limit = 200000000000.0;
  res_out_proof = false;
(*----Combination--------*)
  comb_res_mult = 300000000;
  comb_inst_mult = 1;
  }

 *)

let named_option_epr_horn () =
  { options_name = "Option_epr_horn"; options = (option_epr_horn()) }

(*-----------------------------------------------*)

type ver_epr_opt =
  | Ver_EPR_TABLES_BOUND_3 (* proves rat example bound 3 *)
  | Ver_EPR_TABLES
  | Ver_EPR_Default
  | Ver_EPR_DCU

(* *)
let option_verification_epr ver_epr_opt =
  match ver_epr_opt with
  | Ver_EPR_TABLES_BOUND_3 ->
      {
       (*------------------------------------*)
       
       out_options = !current_options.out_options;
       tptp_safe_out = !current_options.tptp_safe_out;
       
       (*----Input-------*)
       problem_path = !current_options.problem_path;
       include_path = !current_options.include_path;
       problem_files = !current_options.problem_files;
       
       stdin = !current_options.stdin;
       dbg_backtrace = !current_options.dbg_backtrace;
       dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
       dbg_dump_prop_clauses_file =
       !current_options.dbg_dump_prop_clauses_file;
       dbg_out_stat = !current_options.dbg_out_stat;
       
       (*----General--------*)
       fof = false;
       time_out_real = -1.;
       time_out_virtual = -1.;
       schedule = !current_options.schedule;
       ground_splitting = !current_options.ground_splitting;
       non_eq_to_eq = false;
       prep_gs_sim = !current_options.prep_gs_sim;
       prep_res_sim = !current_options.prep_res_sim;
       res_sim_input = !current_options.res_sim_input;
       clause_weak_htbl = !current_options.clause_weak_htbl;
       gc_record_bc_elim = !current_options.gc_record_bc_elim;
       symbol_type_check = !current_options.symbol_type_check;
       clausify_out = false;
       
       clausifier = !current_options.clausifier;
       clausifier_options = !current_options.clausifier_options;
       large_theory_mode = false;
       prep_sem_filter = !current_options.prep_sem_filter;
       prep_sem_filter_out = false;
       (*  sub_typing              = !current_options.sub_typing;*)
       sub_typing = false;
       brand_transform = false;
       min_unsat_core = !current_options.min_unsat_core;
       prolific_symb_bound = 5000;
       lt_threshold = 2000;
       
       (*----Sat Mode--------*)
       sat_mode = false;
       sat_gr_def = false;
       sat_epr_types = !current_options.sat_epr_types;
       sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
       sat_finite_models = false;
       sat_out_model = !current_options.sat_out_model;
       sat_out_clauses = !current_options.sat_out_clauses;
       
       (*----BMC1---------------*)
       bmc1_incremental = ValueDefault true;
       bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
       bmc1_min_bound = ValueDefault 0;
       bmc1_max_bound = ValueDefault (-1);
       bmc1_max_bound_default = ValueDefault (-1);
       bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
       bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_Leaves;
       bmc1_unsat_core_children = ValueDefault false;
       bmc1_unsat_core_extrapolate_axioms = ValueDefault true;
       bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
       bmc1_pre_inst_next_state = false;
       bmc1_pre_inst_state = false;
       bmc1_pre_inst_reach_state = false;
       bmc1_out_unsat_core = ValueDefault false;
       bmc1_verbose = ValueDefault false;
       bmc1_dump_clauses_tptp = ValueDefault false;
       bmc1_dump_unsat_core_tptp = ValueDefault false;
       bmc1_dump_file = ValueDefault None;
       
       (*----Instantiation------*)
       instantiation_flag = true;
       inst_lit_sel = [Lit_Ground true; Lit_Sign false;];
       
       (* before Intel example bpbimodalm_miter_full.focnf.bit_blast.Mclk1 *)
       (* inst_solver_per_active         = 750; after 7500 *)
       (*  inst_solver_per_active         = 750;*)
       (*  inst_solver_per_active         = 7500;*)
       
       inst_solver_per_active = 7500;
       
       (* inst_solver_per_clauses        = 5000; is ok*)
       (*  inst_solver_per_clauses        = 5000;*)
       inst_solver_per_clauses = !current_options.inst_solver_per_clauses;
       
       inst_pass_queue1 =
       ValueDefault [Cl_in_unsat_core true;
		     Cl_Age true;
		     Cl_Num_of_Symb false];
       
       inst_pass_queue1_mult = ValueDefault 20;
       
       inst_pass_queue2 =
       ValueDefault
	 [Cl_Conj_Dist false;
	  Cl_Has_Conj_Symb true;
	  (*			    Cl_Ground true;*)
	  Cl_Num_of_Var false];
       
       inst_pass_queue3 =
       ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
       
       (*"[+age;-num_symb]";*)
       inst_pass_queue2_mult = ValueDefault 25;
       inst_pass_queue3_mult = ValueDefault 20;
       
       (* befor ok inst_dismatching               = false;*)
       inst_dismatching = false;
       (*  inst_dismatching               = false;*)
       (*  inst_dismatching               =  !current_options.inst_dismatching;*)
       
       inst_eager_unprocessed_to_passive = true;
       inst_prop_sim_given = false;
       inst_prop_sim_new = false;
       inst_orphan_elimination = !current_options.inst_orphan_elimination;
       inst_learning_loop_flag = true;
       inst_learning_start = 3000;
       inst_learning_factor = 2;
       inst_start_prop_sim_after_learn = 3000;
       inst_sel_renew = Inst_SR_Solver;
       inst_lit_activity_flag = false;
       inst_out_proof = ValueDefault true;
       
       (*----Resolution----------------------------*)
       resolution_flag = false;
       (*------------------------------------------*)
       res_lit_sel = Res_Adaptive;
       res_to_prop_solver = Res_to_Solver_Active;
       res_prop_simpl_new = false;
       res_prop_simpl_given = false;
       (*switch between simpl and priority queues*)
       (* TO DO  Queues options like in Inst. *)
       res_passive_queue_flag = true;
       res_pass_queue1 = [Cl_Has_Conj_Symb true; ];
       res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
       res_pass_queue1_mult = 15;
       res_pass_queue2_mult = 10;
       
       res_forward_subs = Subs_Subset;
       res_backward_subs = Subs_Subset;
       res_forward_subs_resolution = false;
       res_backward_subs_resolution = false;
       res_orphan_elimination = false;
       res_time_limit = 2.0;
       res_out_proof = !current_options.res_out_proof;
       (*----Combination--------*)
       comb_res_mult = 30;
       comb_inst_mult = 1000;
     }
	
  | Ver_EPR_TABLES | Ver_EPR_Default ->
      {
       (*------------------------------------*)
       
       out_options = !current_options.out_options;
       tptp_safe_out = !current_options.tptp_safe_out;
       
       (*----Input-------*)
       problem_path = !current_options.problem_path;
       include_path = !current_options.include_path;
       problem_files = !current_options.problem_files;
       
       stdin = !current_options.stdin;
       dbg_backtrace = !current_options.dbg_backtrace;
       dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
       dbg_dump_prop_clauses_file =
       !current_options.dbg_dump_prop_clauses_file;
       dbg_out_stat = !current_options.dbg_out_stat;
       
       (*----General--------*)
       fof = false;
       time_out_real = -1.;
       time_out_virtual = -1.;
       schedule = !current_options.schedule;
       ground_splitting = Split_Off;
       non_eq_to_eq = false;
       prep_gs_sim = !current_options.prep_gs_sim;
       prep_res_sim = !current_options.prep_res_sim;
       res_sim_input = !current_options.res_sim_input;
       clause_weak_htbl = !current_options.clause_weak_htbl;
       gc_record_bc_elim = !current_options.gc_record_bc_elim;
       symbol_type_check = !current_options.symbol_type_check;
       clausify_out = false;
       
       clausifier = !current_options.clausifier;
       clausifier_options = !current_options.clausifier_options;
       large_theory_mode = false;
       prep_sem_filter = !current_options.prep_sem_filter;
       prep_sem_filter_out = false;
       (*  sub_typing              = !current_options.sub_typing;*)
       sub_typing = false;
       brand_transform = false;
       min_unsat_core = !current_options.min_unsat_core;
       prolific_symb_bound = 20000000;
       lt_threshold = 20000000;
       
       (*----Sat Mode--------*)
       sat_mode = false;
       sat_gr_def = false;
       sat_epr_types = !current_options.sat_epr_types;
       sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
       sat_finite_models = false;
       sat_out_model = !current_options.sat_out_model;
       sat_out_clauses = !current_options.sat_out_clauses;
       
       (*----BMC1---------------*)
       bmc1_incremental = ValueDefault true;
       bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
       bmc1_min_bound = ValueDefault 0;
       bmc1_max_bound = ValueDefault (-1);
       bmc1_max_bound_default = ValueDefault (-1);
       bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
       bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_Leaves;
       bmc1_unsat_core_children = ValueDefault false;
       bmc1_unsat_core_extrapolate_axioms = ValueDefault true;
       bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
       bmc1_pre_inst_next_state = false;
       bmc1_pre_inst_state = false;
       bmc1_pre_inst_reach_state = false;
       bmc1_out_unsat_core = ValueDefault false;
       bmc1_verbose = ValueDefault false;
       bmc1_dump_clauses_tptp = ValueDefault false;
       bmc1_dump_unsat_core_tptp = ValueDefault false;
       bmc1_dump_file = ValueDefault None;
       
       (*----Instantiation------*)
       instantiation_flag = true;
       inst_lit_sel = [Lit_eq false; Lit_Ground true; Lit_Sign false;];
       
       (* before Intel example bpbimodalm_miter_full.focnf.bit_blast.Mclk1 *)
       (* inst_solver_per_active         = 750; after 7500 *)
       (*  inst_solver_per_active         = 750;*)
       (*  inst_solver_per_active         = 7500;*)
       
       inst_solver_per_active = 7500;
       
       (* inst_solver_per_clauses        = 5000; is ok*)
       (* inst_solver_per_clauses        = 5000;*)
       inst_solver_per_clauses = !current_options.inst_solver_per_clauses;
       
       inst_pass_queue1 =
       ValueDefault
	 [Cl_in_unsat_core true;
	  Cl_Age true;
	  Cl_Num_of_Symb false];
       
       (*
	 inst_pass_queue1 =
	 ValueDefault
	 [Cl_Has_Non_Prolific_Conj_Symb false; Cl_min_defined_symb true;
	 Cl_Age true;
	 Cl_Num_of_Symb false];
	*)
       inst_pass_queue1_mult = ValueDefault 20;
       
       inst_pass_queue2 =
       ValueDefault
	 [Cl_Conj_Dist false;
	  Cl_Has_Conj_Symb true;
	  (*			    Cl_Ground true;*)
	  Cl_Num_of_Var false];
       
       inst_pass_queue3 =
       ValueDefault [Cl_Age true; Cl_Num_of_Symb false];
       
       (*"[+age;-num_symb]";*)
       
       inst_pass_queue2_mult = ValueDefault 25;
       inst_pass_queue3_mult = ValueDefault 20;
       
       (* befor ok inst_dismatching               = false;*)
       (*  inst_dismatching               = false;*)
       inst_dismatching = false;
       (*  inst_dismatching               =  !current_options.inst_dismatching;*)
       
       inst_eager_unprocessed_to_passive = true;
       inst_prop_sim_given = false;
       inst_prop_sim_new = false;
       inst_orphan_elimination = !current_options.inst_orphan_elimination;
       inst_learning_loop_flag = true;
       (* inst_learning_start               = 1000;*)
       inst_learning_start = 100000;
       inst_learning_factor = 10;
       inst_start_prop_sim_after_learn = 300000000;
       inst_sel_renew = Inst_SR_Solver;
       inst_lit_activity_flag = false;
       inst_out_proof = ValueDefault true;
       
       (*----Resolution----------------------------*)
       resolution_flag = false;
       (*------------------------------------------*)
       res_lit_sel = Res_Adaptive;
       res_to_prop_solver = Res_to_Solver_Active;
       res_prop_simpl_new = false;
       res_prop_simpl_given = false;
       (*switch between simpl and priority queues*)
       (* TO DO  Queues options like in Inst. *)
       res_passive_queue_flag = true;
       res_pass_queue1 = [Cl_Has_Conj_Symb true; ];
       res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
       res_pass_queue1_mult = 15;
       res_pass_queue2_mult = 10;
       
       res_forward_subs = Subs_Subset;
       res_backward_subs = Subs_Subset;
       res_forward_subs_resolution = false;
       res_backward_subs_resolution = false;
       res_orphan_elimination = false;
       res_time_limit = 2.0;
       res_out_proof = !current_options.res_out_proof;
       (*----Combination--------*)
       comb_res_mult = 30;
       comb_inst_mult = 10000;
     }
  | Ver_EPR_DCU ->
      {
       (*------------------------------------*)
       (* all general options are take from  !current_options anyway since *)
       (* schedule becomes effective only during proof search not during preprocessing  *)
       (* in particular sub_typing false should be added to the input option for bmc1 *)
       out_options = !current_options.out_options;
       tptp_safe_out = !current_options.tptp_safe_out;
       
       (*----Input-------*)
       problem_path = !current_options.problem_path;
       include_path = !current_options.include_path;
       problem_files = !current_options.problem_files;
       
       stdin = !current_options.stdin;
       dbg_backtrace = !current_options.dbg_backtrace;
       dbg_dump_prop_clauses = !current_options.dbg_dump_prop_clauses;
       dbg_dump_prop_clauses_file =
       !current_options.dbg_dump_prop_clauses_file;
       dbg_out_stat = !current_options.dbg_out_stat;
       
       (*----General--------*)
       fof = false;
       time_out_real = -1.;
       time_out_virtual = -1.;
       schedule = !current_options.schedule;
       ground_splitting = Split_Input;
       non_eq_to_eq = false;
       prep_gs_sim = !current_options.prep_gs_sim;
       prep_res_sim = !current_options.prep_res_sim;
       res_sim_input = !current_options.res_sim_input;
       clause_weak_htbl = !current_options.clause_weak_htbl;
       gc_record_bc_elim = !current_options.gc_record_bc_elim;
       symbol_type_check = !current_options.symbol_type_check;
       clausify_out = false;
       
       clausifier = !current_options.clausifier;
       clausifier_options = !current_options.clausifier_options;
       large_theory_mode = false;
       (* prep_sem_filter         = !current_options.prep_sem_filter;  does not work correctly with bmc*)
       prep_sem_filter = Sem_Filter_None;
       prep_sem_filter_out = false;
       (*       sub_typing              = !current_options.sub_typing;*)
       sub_typing = false;
       brand_transform = false;
       min_unsat_core = !current_options.min_unsat_core;
       prolific_symb_bound = 5000;
       lt_threshold = 2000;
       
       (*----Sat Mode--------*)
       sat_mode = false;
       sat_gr_def = false;
       sat_epr_types = !current_options.sat_epr_types;
       sat_non_cyclic_types = !current_options.sat_non_cyclic_types;
       sat_finite_models = false;
       sat_out_model = !current_options.sat_out_model;
       sat_out_clauses = !current_options.sat_out_clauses;
       
       (*----BMC1---------------*)
       bmc1_incremental = ValueDefault true;
       bmc1_axioms = ValueDefault BMC1_Axioms_Reachable_All;
       bmc1_min_bound = ValueDefault 0;
       bmc1_max_bound = ValueDefault (-1);
       bmc1_max_bound_default = ValueDefault (-1);
       (*  bmc1_symbol_reachability should always be taken from !current_options.bmc1_symbol_reachability *)
       bmc1_symbol_reachability = !current_options.bmc1_symbol_reachability;
       bmc1_add_unsat_core = ValueDefault BMC1_Add_Unsat_Core_Leaves;
       bmc1_unsat_core_children = ValueDefault false;
       bmc1_unsat_core_extrapolate_axioms = ValueDefault true;
       bmc1_out_stat = ValueDefault BMC1_Out_Stat_Full;
       (* these should always be assigned to the input options *)
       (* since initial partial instantiation is done based on current_options,*)
       (* before schedule options take effect *)
       bmc1_pre_inst_next_state = !current_options.bmc1_pre_inst_next_state;
       bmc1_pre_inst_state = !current_options.bmc1_pre_inst_state;
       bmc1_pre_inst_reach_state = !current_options.bmc1_pre_inst_reach_state;
       bmc1_out_unsat_core = ValueDefault false;
       bmc1_verbose = ValueDefault false;
       bmc1_dump_clauses_tptp = ValueDefault false;
       bmc1_dump_unsat_core_tptp = ValueDefault false;
       bmc1_dump_file = ValueDefault None;
       
       (*----Instantiation------*)
       instantiation_flag = true;
       
       (*
	 inst_lit_sel = [Lit_Ground true; Lit_Sign false;];
	*)
       (* usual *)
       inst_lit_sel =
       [
	
	Lit_clock true;
	(* Lit_reachable_state true;
	   Lit_next_state true;*)
	Lit_Ground true;
	Lit_Sign false; ];
       
       (*
	 inst_lit_sel =
	 [
	 Lit_next_state false;
	 Lit_clock true;
	 (* Lit_reachable_state true;
	    Lit_next_state true;*)
	 Lit_Ground true;
	 Lit_Sign false; ];
	*)
       
       (*     inst_lit_sel                   = [Lit_Sign false;];*)
       (* before Intel example bpbimodalm_miter_full.focnf.bit_blast.Mclk1 *)
       (* inst_solver_per_active         = 750; after 7500 *)
       (*  inst_solver_per_active         = 750;*)
       (*  inst_solver_per_active         = 7500;*)
       
       (*       inst_solver_per_active         = 25000;*)
       inst_solver_per_active = 25000;
       
       (* inst_solver_per_clauses        = 5000; is ok*)
       (*  inst_solver_per_clauses        = 5000;*)
       inst_solver_per_clauses = !current_options.inst_solver_per_clauses;
       
       inst_pass_queue1 =
       ValueDefault
	 [
	  Cl_in_unsat_core true;
	  (*	     Cl_has_reachable_state true;*)
	  (*	Cl_min_defined_symb false; *)
	  (* Cl_has_next_state true;
	     Cl_has_reachable_state true;*)
	  (*	     Cl_Has_Eq_Lit false;*)
	  Cl_Conj_Dist false;
	  Cl_Age true;
	  Cl_Num_of_Symb false];
       
       inst_pass_queue1_mult = ValueDefault 20;
       
       inst_pass_queue2 =
       (*
	 [Cl_Conj_Dist false;
	 Cl_Has_Conj_Symb true;
	 (*Cl_min_defined_symb false;	Cl_has_bound_constant true;*) (*Cl_Has_Eq_Lit false;*)
	 (*			    Cl_Ground true;*)
	 Cl_Num_of_Var false];
	*)
       (*[Cl_min_defined_symb false; Cl_Age true; Cl_Num_of_Symb false];
	*)
       
       ValueDefault
	 [
	  
	  (*		Cl_min_defined_symb false;*)
	  Cl_Conj_Dist false;
	  Cl_Has_Eq_Lit false;
	  (*	Cl_Has_Conj_Symb true; *)
	  Cl_has_bound_constant true;
	  
	  (* Cl_Ground true;*)
	  Cl_Num_of_Var false;
	  (* Cl_min_defined_symb false;*)
	];
       inst_pass_queue2_mult = ValueDefault 25;
       
       (*     inst_pass_queue2               = [Cl_Age true; Cl_Num_of_Symb false];*)
       
       inst_pass_queue3 =
       ValueDefault
	 [
	  Cl_Age true;
	  Cl_min_defined_symb false;
	  (*Cl_min_defined_symb false;*)
	  Cl_Num_of_Symb false ];
       
       (*"[+age;-num_symb]";*)
       (*       inst_pass_queue1_mult          = 100;*)
       
       inst_pass_queue3_mult = ValueDefault 20;
       (*
	 inst_pass_queue1_mult = !current_options.inst_pass_queue1_mult;
	 inst_pass_queue2_mult = !current_options.inst_pass_queue2_mult;
	*)
       
       (* befor ok inst_dismatching               = false;*)
       (*       inst_dismatching               = false;*)
       inst_dismatching = true;
       (*  inst_dismatching               =  !current_options.inst_dismatching;*)
       
       inst_eager_unprocessed_to_passive = true;
       
       (*    inst_prop_sim_given               = !current_options.inst_prop_sim_given; (*change to false*) *)
       inst_prop_sim_given = false;
       
       inst_prop_sim_new = false;
       inst_orphan_elimination = !current_options.inst_orphan_elimination;
       (*     inst_prop_sim_new                 = true;*)
       inst_learning_loop_flag = true;
       (*       inst_learning_loop_flag           = false; *)
       inst_learning_start = 30000;
       inst_learning_factor = 3;
       inst_start_prop_sim_after_learn = 0;
       inst_sel_renew = Inst_SR_Solver;
       inst_lit_activity_flag = false;
       (*    inst_lit_activity_flag            = true;*)
       inst_out_proof = ValueDefault true;
       
       (*----Resolution----------------------------*)
       resolution_flag = false;
       (*------------------------------------------*)
       res_lit_sel = Res_Adaptive;
       res_to_prop_solver = Res_to_Solver_Active;
       res_prop_simpl_new = false;
       res_prop_simpl_given = false;
       (*switch between simpl and priority queues*)
       (* TO DO  Queues options like in Inst. *)
       res_passive_queue_flag = true;
       res_pass_queue1 = [Cl_Has_Conj_Symb true; ];
       res_pass_queue2 = [Cl_Age true; Cl_Num_of_Symb false];
       res_pass_queue1_mult = 15;
       res_pass_queue2_mult = 10;
       
       res_forward_subs = Subs_Subset;
       res_backward_subs = Subs_Subset;
       res_forward_subs_resolution = false;
       res_backward_subs_resolution = false;
       res_orphan_elimination = false;
       res_time_limit = 2.0;
       res_out_proof = !current_options.res_out_proof;
       (*----Combination--------*)
       comb_res_mult = 30;
       comb_inst_mult = 1000;
     }

let named_option_verification_epr () =
  { options_name = "Option_verification_epr";
    (*   options = (option_verification_epr Ver_EPR_TABLES_BOUND_3)*)
    options = (option_verification_epr Ver_EPR_DCU)
      (*was Ver_EPR_DCU when in June 8th 2012*)
      (*  options = (option_verification_epr Ver_EPR_Default)*)
  }

let named_option_verification_epr_tables () =
  { options_name = "Option_verification_epr_tables";
    options = (option_verification_epr Ver_EPR_TABLES) }
